1 /-
2 Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Author: Sébastien Gouëzel
5 -/
6
7 import topology.metric_space.isometry topology.instances.ennreal
src └────────────────────────────┘ └────────────────────────┘
8 topology.metric_space.lipschitz
src └─────────────────────────────┘
9
10 /-!
11 # Hausdorff distance
12
13 The Hausdorff distance on subsets of a metric (or emetric) space.
14
15 Given two subsets `s` and `t` of a metric space, their Hausdorff distance is the smallest `d`
16 such that any point `s` is within `d` of a point in `t`, and conversely. This quantity
17 is often infinite (think of `s` bounded and `t` unbounded), and therefore better
18 expressed in the setting of emetric spaces.
19
20 ## Main definitions
21
22 This files introduces:
23 * `inf_edist x s`, the infimum edistance of a point `x` to a set `s` in an emetric space
24 * `Hausdorff_edist s t`, the Hausdorff edistance of two sets in an emetric space
25 * Versions of these notions on metric spaces, called respectively `inf_dist` and
26 `Hausdorff_dist`.
27 -/
28 noncomputable theory
29 open_locale classical
30 universes u v w
31
32 open classical lattice set function topological_space filter
33
34 namespace emetric
35
36 section inf_edist
37 open_locale ennreal
38 variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β] {x y : α} {s t : set α} {Φ : α → β}
id └───────────┘ └───────────┘ └─┘
src └───────────┘ └───────────┘ └─┘
typ └───────────┘ └───────────┘ └─┘
doc └───────────┘ └───────────┘
39
40 /-- The minimal edistance of a point to a set -/
41 def inf_edist (x : α) (s : set α) : ennreal := Inf ((edist x) '' s)
id ┴ └─┘ ┴ └─────┘ └─┘ └───┘ ┴ └┘ ┴
src └─┘ └─────┘ └─┘ └───┘ └┘
typ ┴ └─┘ ┴ └─────┘ └─┘ └───┘ ┴ └┘ ┴
doc └─────┘ └─┘
42
43 @[simp] lemma inf_edist_empty : inf_edist x ∅ = ∞ :=
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
doc └──┘ └───────┘ ┴
44 by unfold inf_edist; simp
src └──────────────┘ └────
typ └──────────────┘ └────
doc └──────────────┘ └────
txt └──────────────┘ └────
par └──────────────┘ └────
pid └────────┘ └
st └───────────────────────
45
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
46 /-- The edist to a union is the minimum of the edists -/
47 @[simp] lemma inf_edist_union : inf_edist x (s ∪ t) = inf_edist x s ⊓ inf_edist x t :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └──┘ └───────┘ └───────┘ └───────┘
48 by simp [inf_edist, image_union, Inf_union]
src └────┘ └┘ └┘ └─
typ └────┘ └┘ └┘ └─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
50 /-- The edist to a singleton is the edistance to the single point of this singleton -/
51 @[simp] lemma inf_edist_singleton : inf_edist x {y} = edist x y :=
doc └──┘
52 by simp [inf_edist]
src └────┘ └─
typ └────┘ └─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
53
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
54 /-- The edist to a set is bounded above by the edist to any of its points -/
55 lemma inf_edist_le_edist_of_mem (h : y ∈ s) : inf_edist x s ≤ edist x y :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
src ┴ └───────┘ ┴ └───┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───────┘
56 Inf_le ((mem_image _ _ _).2 ⟨y, h, by refl⟩)
id └────┘ └───────┘ ┴ ┴ ┴
src └────┘ └───────┘ ┴ └──┘
typ └────┘ └───────┘ ┴ ┴ ┴ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
57
58 /-- If a point `x` belongs to `s`, then its edist to `s` vanishes -/
59 lemma inf_edist_zero_of_mem (h : x ∈ s) : inf_edist x s = 0 :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src ┴ └───────┘ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘
60 le_zero_iff_eq.1 $ @edist_self _ _ x ▸ inf_edist_le_edist_of_mem h
id └────────────┘┴ └────────┘ ┴ ┴ └───────────────────────┘ ┴
src └────────────┘┴ └────────┘ ┴ └───────────────────────┘
typ └────────────┘┴ └────────┘ ┴ ┴ └───────────────────────┘ ┴
doc └───────────────────────┘
61
62 /-- The edist is monotonous with respect to inclusion -/
63 lemma inf_edist_le_inf_edist_of_subset (h : s ⊆ t) : inf_edist x t ≤ inf_edist x s :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
src ┴ └───────┘ ┴ └───────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └───────┘
64 Inf_le_Inf (image_subset _ h)
id └────────┘ └──────────┘ ┴
src └────────┘ └──────────┘
typ └────────┘ └──────────┘ ┴
65
66 /-- If the edist to a set is `< r`, there exists a point in the set at edistance `< r` -/
67 lemma exists_edist_lt_of_inf_edist_lt {r : ennreal} (h : inf_edist x s < r) :
id └─────┘ └───────┘ ┴ ┴ ┴ ┴
src └─────┘ └───────┘ ┴
typ └─────┘ └───────┘ ┴ ┴ ┴ ┴
doc └─────┘ └───────┘
68 ∃y∈s, edist x y < r :=
id ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴
typ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
69 let ⟨t, ⟨ht, tr⟩⟩ := Inf_lt_iff.1 h in
id └─┘ └┘ └────────┘┴ ┴
src └────────┘┴
typ └─┘ └┘ └────────┘┴ ┴
70 let ⟨y, ⟨ys, hy⟩⟩ := (mem_image _ _ _).1 ht in
id └─┘ ┴ └┘ └───────┘ ┴
src └───────┘ ┴
typ └─┘ ┴ └┘ └───────┘ ┴
71 ⟨y, ys, by rwa ← hy at tr⟩
id └┘
src └────┘ └────┘
typ └────┘└┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid └─┘ └────┘
st └─────────────┘
72
73 /-- The edist of `x` to `s` is bounded by the sum of the edist of `y` to `s` and
74 the edist from `x` to `y` -/
75 lemma inf_edist_le_inf_edist_add_edist : inf_edist x s ≤ inf_edist y s + edist x y :=
id └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ └───┘
typ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └───┘ ┴ ┴
doc └───────┘ └───────┘
76 begin
st └─────
77 have : ∀z ∈ s, Inf (edist x '' s) ≤ edist y z + edist x y := λz hz, calc
id └─┘ └┘ ┴ ┴ ┴ └───┘ ┴ ┴
src └─────┘ └──┘ ┴└─┘┴ ┴ ┴└┘┴ └┘┴┴ ┴ ┴ ┴┴┴└───┘┴ ┴ └──┘ └────┘ └
typ └─────┘ └──┘ ┴└─┘┴ ┴ ┴└┘┴┴└┘┴┴ ┴ ┴ ┴┴┴└───┘┴┴┴┴└──┘ └────┘ └
doc └─────┘ └──┘ ┴└─┘┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
txt └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
par └─────┘ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
pid └───┘└┘ └──┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ └────┘ └
st ───────────────────────────────────────────────────────────────────────────
78 Inf (edist x '' s) ≤ edist x z :
id └─┘ ┴ └───┘ ┴
src ───┘└─┘┴ ┴ ┴ ┴ └┘ ┴└───┘┴ ┴ └──
typ ───┘└─┘┴ ┴ ┴ ┴┴└┘ ┴└───┘┴┴┴ └──
doc ───┘└─┘┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
txt ───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
par ───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
pid ───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──
st ─────────────────────────────────────
79 Inf_le ((mem_image _ _ _).2 ⟨z, hz, by refl⟩)
id └────┘ └───────┘
src ─────┘└────┘┴ └───────┘└────────┘ └┘ └┘ ┴└──┘└──
typ ─────┘└────┘┴ └───────┘└────────┘ └┘ └┘ ┴└──┘└──
doc ─────┘ ┴ └────────┘ └┘ └┘ ┴└──┘└──
txt ─────┘ ┴ └────────┘ └┘ └┘ ┴└──┘└──
par ─────┘ ┴ └────────┘ └┘ └┘ ┴└──┘└──
pid ─────┘ ┴ └────────┘ └┘ └┘ └───────
st ───────────────────────────────────────────┘└───┘└──
80 ... ≤ edist x y + edist y z : edist_triangle _ _ _
id └────────────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────┘└──────
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────┘└──────
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──────
st ───────────────────────────────────────────────────────
81 ... = edist y z + edist x y : add_comm _ _,
id ┴ └──────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘└──────┘└──┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└─┘└──────┘└──┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └──┘
st ─────────────────────────────────────────────┘└─
82 have : (λz, z + edist x y) (Inf (edist y '' s)) = Inf ((λz, z + edist x y) '' (edist y '' s)),
id ┴ └─┘ ┴ └───┘ ┴ ┴
src └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘┴┴└─┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ └───┘┴ ┴ ┴ └┘
typ └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘┴┴└─┘┴ └─┘ ┴ ┴ ┴┴┴ └┘ ┴ └───┘┴┴┴ ┴┴└┘
doc └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴└─┘┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
txt └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
par └─────┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
pid └───┘└┘ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘
st ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
83 { refine Inf_of_continuous _ _ (by simp),
id └───────────────┘
src └─────┘└───────────────┘└───┘ ┴└──┘┴
typ └─────┘└───────────────┘└───┘ ┴└──┘┴
doc └─────┘└───────────────┘└───┘ ┴└──┘┴
txt └─────┘ └───┘ ┴└──┘┴
par └─────┘ └───┘ ┴└──┘┴
pid ┴ └───┘ └────┘
st ───┘└──────────────────────────────┘└───┘┴└─
84 { exact continuous_id.add continuous_const },
id └───────────────┘ └──────────────┘
src └────┘└───────────────┘┴└──────────────┘┴
typ └────┘└───────────────┘┴└──────────────┘┴
doc └────┘ ┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ─────┘└───────────────────────────────────────┘└┘└
85 { assume a b h, simp, apply add_le_add_right' h }},
id └───────────────┘ ┴
src └──────────┘ └──┘ └────┘└───────────────┘┴ ┴
typ └──────────┘ └──┘ └────┘└───────────────┘┴┴┴
doc └──────────┘ └──┘ └────┘ ┴ ┴
txt └──────────┘ └──┘ └────┘ ┴ ┴
par └──────────┘ └──┘ └────┘ ┴ ┴
pid └──────────┘ ┴ ┴ ┴
st ─────────────────┘└────┘└──────────────────────────┘└─┘└
86 simp only [inf_edist] at this,
id └───────┘
src └─────────┘└───────┘└───────┘
typ └─────────┘└───────┘└───────┘
doc └─────────┘└───────┘└───────┘
txt └─────────┘ └───────┘
par └─────────┘ └───────┘
pid ┴└──┘└┘ ┴┴└─────┘
st ──────────────────────────────┘└─
87 rw [inf_edist, inf_edist, this, ← image_comp],
id └───────┘ └───────┘ └──┘ └────────┘
src └──┘└───────┘└┘└───────┘└┘ └──┘└────────┘┴
typ └──┘└───────┘└┘└───────┘└┘└──┘└──┘└────────┘┴
doc └──┘└───────┘└┘└───────┘└┘ └──┘ ┴
txt └──┘ └┘ └┘ └──┘ ┴
par └──┘ └┘ └┘ └──┘ ┴
pid └┘ └┘ └┘ └──┘ ┴
st ──────────────┘└─────────┘└────┘└────────────┘└──
88 simpa only [and_imp, function.comp_app, lattice.le_Inf_iff, exists_imp_distrib, ball_image_iff]
id └─────┘ └───────────────┘ └────────────────┘ └────────────────┘ └────────────┘
src └──────────┘└─────┘└┘└───────────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────┘└┘
typ └──────────┘└─────┘└┘└───────────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────┘└┘
doc └──────────┘ └┘ └┘ └┘ └┘ └┘
txt └──────────┘ └┘ └┘ └┘ └┘ └┘
par └──────────┘ └┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────┘
89 end
st └─┘
90
91 /-- The edist to a set depends continuously on the point -/
92 lemma continuous_inf_edist : continuous (λx, inf_edist x s) :=
id └────────┘ ┴ └───────┘ ┴ ┴
src └────────┘ └───────┘
typ └────────┘ ┴ └───────┘ ┴ ┴
doc └────────┘ └───────┘
93 continuous_of_le_add_edist 1 (by simp) $
id └────────────────────────┘
src └────────────────────────┘ └──┘
typ └────────────────────────┘ └──┘
doc └──┘
txt └──┘
par └──┘
st └───┘
94 by simp only [one_mul, inf_edist_le_inf_edist_add_edist, forall_2_true_iff]
id └─────┘ └──────────────────────────────┘ └───────────────┘
src └─────────┘└─────┘└┘└──────────────────────────────┘└┘└───────────────┘└─
typ └─────────┘└─────┘└┘└──────────────────────────────┘└┘└───────────────┘└─
doc └─────────┘ └┘└──────────────────────────────┘└┘ └─
txt └─────────┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────────────────
95
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
96 /-- The edist to a set and to its closure coincide -/
97 lemma inf_edist_closure : inf_edist x (closure s) = inf_edist x s :=
id └───────┘ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └─────┘ ┴ └───────┘
typ └───────┘ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └─────┘ └───────┘
98 begin
st └─────
99 refine le_antisymm (inf_edist_le_inf_edist_of_subset subset_closure) _,
id └─────────┘ └──────────────────────────────┘ └────────────┘
src └─────┘└─────────┘┴ └──────────────────────────────┘┴└────────────┘└─┘
typ └─────┘└─────────┘┴ └──────────────────────────────┘┴└────────────┘└─┘
doc └─────┘ ┴ └──────────────────────────────┘┴ └─┘
txt └─────┘ ┴ ┴ └─┘
par └─────┘ ┴ ┴ └─┘
pid ┴ ┴ ┴ └─┘
st ───────────────────────────────────────────────────────────────────────┘└─
100 refine ennreal.le_of_forall_epsilon_le (λε εpos h, _),
id └─────────────────────────────┘
src └─────┘└─────────────────────────────┘┴ └──────────┘
typ └─────┘└─────────────────────────────┘┴ └──────────┘
doc └─────┘ ┴ └──────────┘
txt └─────┘ ┴ └──────────┘
par └─────┘ ┴ └──────────┘
pid ┴ ┴ └──────────┘
st ──────────────────────────────────────────────────────┘└─
101 have εpos' : (0 : ennreal) < ε := by simpa,
id └─────┘ ┴ ┴
src └───────────┘ └──┘└─────┘└┘┴┴ └──┘ ┴└───┘
typ └───────────┘ └──┘└─────┘└┘┴┴┴└──┘ ┴└───┘
doc └───────────┘ └──┘└─────┘└┘ ┴ └──┘ ┴└───┘
txt └───────────┘ └──┘ └┘ ┴ └──┘ ┴└───┘
par └───────────┘ └──┘ └┘ ┴ └──┘ ┴└───┘
pid └────────┘└─┘ └──┘ └┘ ┴ └──┘ └────┘
st ─────────────────────────────────────┘└────┘└─
102 have : inf_edist x (closure s) < inf_edist x (closure s) + ε/2 :=
id └───────┘ ┴ └─────┘ ┴ ┴ ┴┴
src └─────┘ ┴ ┴ ┴ └┘ ┴└───────┘┴ ┴ └─────┘┴ └┘┴┴ ┴└────
typ └─────┘ ┴ ┴ ┴ └┘ ┴└───────┘┴┴┴ └─────┘┴┴└┘┴┴┴┴└────
doc └─────┘ ┴ ┴ ┴ └┘ ┴└───────┘┴ ┴ └─────┘┴ └┘ ┴ └────
txt └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
par └─────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
pid └───┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ └┘ ┴ └────
st ────────────────────────────────────────────────────────────────────
103 ennreal.lt_add_right h (ennreal.half_pos εpos'),
id └──────────────────┘ ┴ └──────────────┘ └───┘
src ───┘└──────────────────┘┴ ┴ └──────────────┘┴ ┴
typ ───┘└──────────────────┘┴┴┴ └──────────────┘┴└───┘┴
doc ───┘ ┴ ┴ ┴ ┴
txt ───┘ ┴ ┴ ┴ ┴
par ───┘ ┴ ┴ ┴ ┴
pid ───┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────┘└─
104 rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ycs, hy⟩,
id └─────────────────────────────┘ └──┘
src └─────┘└─────────────────────────────┘┴ └────────────────┘
typ └─────┘└─────────────────────────────┘┴└──┘└────────────────┘
doc └─────┘└─────────────────────────────┘┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
105 -- y : α, ycs : y ∈ closure s, hy : edist x y < inf_edist x (closure s) + ↑ε / 2
st ──────────────┘┴└────────────────────────────────────────────────────────────────────
106 rcases emetric.mem_closure_iff'.1 ycs (ε/2) (ennreal.half_pos εpos') with ⟨z, zs, dyz⟩,
id └──────────────────────┘ └─┘ ┴ └──────────────┘ └───┘
src └─────┘└──────────────────────┘└─┘ ┴ └─┘ └──────────────┘┴ └─────────────────┘
typ └─────┘└──────────────────────┘└─┘└─┘┴ ┴ └─┘ └──────────────┘┴└───┘└─────────────────┘
doc └─────┘└──────────────────────┘└─┘ ┴ └─┘ ┴ └─────────────────┘
txt └─────┘ └─┘ ┴ └─┘ ┴ └─────────────────┘
par └─────┘ └─┘ ┴ └─┘ ┴ └─────────────────┘
pid ┴ └─┘ ┴ └─┘ ┴ └─────────────────┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
107 -- z : α, zs : z ∈ s, dyz : edist y z < ↑ε / 2
st ───────────────────────────────────────────────────
108 calc inf_edist x s ≤ edist x z : inf_edist_le_edist_of_mem zs
id └──┘ └───┘ ┴ ┴ └───────────────────────┘ └┘
src └──┘ └───┘ └───────────────────────┘
typ └──┘ └───┘ ┴ ┴ └───────────────────────┘ └┘
doc └──┘ └───────────────────────┘
st ────────────────────────────────────────────────────────────────
109 ... ≤ edist x y + edist y z : edist_triangle _ _ _
id ┴ └────────────┘
src └────────────┘
typ ┴ └────────────┘
st ───────────────────────────────────────────────────────────
110 ... ≤ (inf_edist x (closure s) + ε / 2) + (ε/2) : add_le_add' (le_of_lt hy) (le_of_lt dyz)
id └─────────┘ └┘ └──────┘ └─┘
src └─────────┘ └──────┘
typ └─────────┘ └┘ └──────┘ └─┘
st ───────────────────────────────────────────────────────────────────────────────────────────────────
111 ... = inf_edist x (closure s) + ↑ε : by simp [ennreal.add_halves]
id └───────┘ └─────┘ ┴ ┴┴ └────────────────┘
src └───────┘ └─────┘ ┴ └────┘└────────────────┘└┘
typ └───────┘ └─────┘ ┴ ┴┴ └────┘└────────────────┘└┘
doc └───────┘ └─────┘ └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ──────────────────────────────────────────────┘└─────────────────────────┘
112 end
st └─┘
113
114 /-- A point belongs to the closure of `s` iff its infimum edistance to this set vanishes -/
115 lemma mem_closure_iff_inf_edist_zero : x ∈ closure s ↔ inf_edist x s = 0 :=
id ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴ ┴
src ┴ └─────┘ ┴ └───────┘ ┴
typ ┴ ┴ └─────┘ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └─────┘ └───────┘
116 ⟨λh, by rw ← inf_edist_closure; exact inf_edist_zero_of_mem h,
id ┴ └───────────────┘ └───────────────────┘ ┴
src └───┘└───────────────┘ └────┘└───────────────────┘┴
typ ┴ └───┘└───────────────┘ └────┘└───────────────────┘┴┴
doc └───┘└───────────────┘ └────┘└───────────────────┘┴
txt └───┘ └────┘ ┴
par └───┘ └────┘ ┴
pid └─┘ ┴ ┴
st └────────────────────────────────────────────────────┘
117 λh, emetric.mem_closure_iff'.2 $ λε εpos, exists_edist_lt_of_inf_edist_lt (by rwa h)⟩
id ┴ └──────────────────────┘┴ ┴ └──┘ └─────────────────────────────┘ ┴
src └──────────────────────┘┴ └─────────────────────────────┘ └──┘
typ ┴ └──────────────────────┘┴ ┴ └──┘ └─────────────────────────────┘ └──┘┴
doc └──────────────────────┘ └─────────────────────────────┘ └──┘
txt └──┘
par └──┘
pid ┴
st └────┘
118
119 /-- Given a closed set `s`, a point belongs to `s` iff its infimum edistance to this set vanishes -/
120 lemma mem_iff_ind_edist_zero_of_closed (h : is_closed s) : x ∈ s ↔ inf_edist x s = 0 :=
id └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └───────┘ ┴ ┴ └───────┘ ┴
typ └───────┘ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └───────┘ └───────┘
121 begin
st └─────
122 convert ← mem_closure_iff_inf_edist_zero,
id └────────────────────────────┘
src └────────┘└────────────────────────────┘
typ └────────┘└────────────────────────────┘
doc └────────┘└────────────────────────────┘
txt └────────┘
par └────────┘
pid └┘┴
st ─────────────────────────────────────────┘└─
123 exact closure_eq_iff_is_closed.2 h
id └──────────────────────┘ ┴
src └────┘└──────────────────────┘└─┘ ┴
typ └────┘└──────────────────────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────────────┘
124 end
st └─┘
125
126 /-- The infimum edistance is invariant under isometries -/
127 lemma inf_edist_image (hΦ : isometry Φ) :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
128 inf_edist (Φ x) (Φ '' t) = inf_edist x t :=
id └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ └┘ ┴ └───────┘
typ └───────┘ ┴ ┴ ┴ └┘ ┴ ┴ └───────┘ ┴ ┴
doc └───────┘ └───────┘
129 begin
st └─────
130 simp only [inf_edist],
id └───────┘
src └─────────┘└───────┘┴
typ └─────────┘└───────┘┴
doc └─────────┘└───────┘┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid ┴└──┘└┘ ┴
st ──────────────────────┘└─
131 apply congr_arg,
id └───────┘
src └────┘└───────┘
typ └────┘└───────┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ────────────────┘└─
132 ext b, split,
src └───┘ └───┘
typ └───┘ └───┘
doc └───┘ └───┘
txt └───┘ └───┘
par └───┘ └───┘
pid └┘
st ──────┘└─────┘└─
133 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ───┘└───────┘└─
134 rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└────────┘ └──────────────────┘
typ └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc └─────┘ └────────┘ └──────────────────┘
txt └─────┘ └────────┘ └──────────────────┘
par └─────┘ └────────┘ └──────────────────┘
pid ┴ └────────┘ └──────────────────┘
st ────────────────────────────────────────────────────┘└─
135 rcases (mem_image _ _ _).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└────────┘ └──────────────────┘
typ └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc └─────┘ └────────┘ └──────────────────┘
txt └─────┘ └────────┘ └──────────────────┘
par └─────┘ └────────┘ └──────────────────┘
pid ┴ └────────┘ └──────────────────┘
st ────────────────────────────────────────────────────┘└─
136 rw [← hy', ← hz', hΦ x z],
id └─┘ └─┘ └┘ ┴ ┴
src └────┘ └──┘ └┘ ┴ ┴ ┴
typ └────┘└─┘└──┘└─┘└┘└┘┴┴┴┴┴
doc └────┘ └──┘ └┘ ┴ ┴ ┴
txt └────┘ └──┘ └┘ ┴ ┴ ┴
par └────┘ └──┘ └┘ ┴ ┴ ┴
pid └──┘ └──┘ └┘ ┴ ┴ ┴
st ────────────┘└─────┘└──────┘└──
137 exact mem_image_of_mem _ hz },
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ───────────────────────────────┘└┘└
138 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ────────────┘└─
139 rcases (mem_image _ _ _).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└────────┘ └──────────────────┘
typ └─────┘ └───────┘└────────┘└┘└──────────────────┘
doc └─────┘ └────────┘ └──────────────────┘
txt └─────┘ └────────┘ └──────────────────┘
par └─────┘ └────────┘ └──────────────────┘
pid ┴ └────────┘ └──────────────────┘
st ────────────────────────────────────────────────────┘└─
140 rw [← hy', ← hΦ x y],
id └─┘ └┘ ┴ ┴
src └────┘ └──┘ ┴ ┴ ┴
typ └────┘└─┘└──┘└┘┴┴┴┴┴
doc └────┘ └──┘ ┴ ┴ ┴
txt └────┘ └──┘ ┴ ┴ ┴
par └────┘ └──┘ ┴ ┴ ┴
pid └──┘ └──┘ ┴ ┴ ┴
st ────────────┘└────────┘└──
141 exact mem_image_of_mem _ (mem_image_of_mem _ hy) }
id └──────────────┘ └┘
src └────┘ └─┘ └──────────────┘└─┘ └┘
typ └────┘ └─┘ └──────────────┘└─┘└┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ────────────────────────────────────────────────────┘└─
142 end
st ──┘
143
144 end inf_edist --section
145
146 /-- The Hausdorff edistance between two sets is the smallest `r` such that each set
147 is contained in the `r`-neighborhood of the other one -/
148 def Hausdorff_edist {α : Type u} [emetric_space α] (s t : set α) : ennreal :=
id └───────────┘ ┴ └─┘ ┴ └─────┘
src └───────────┘ └─┘ └─────┘
typ └───────────┘ ┴ └─┘ ┴ └─────┘
doc └───────────┘ └─────┘
149 Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t)
id └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴
src └─┘ └───────┘ └┘ ┴ └─┘ └───────┘ └┘
typ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴
doc └─┘ └───────┘ └─┘ └───────┘
150
151 lemma Hausdorff_edist_def {α : Type u} [emetric_space α] (s t : set α) :
id └───────────┘ ┴ └─┘ ┴
src └───────────┘ └─┘
typ └───────────┘ ┴ └─┘ ┴
doc └───────────┘
152 Hausdorff_edist s t = Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) := rfl
id └─────────────┘ ┴ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └─┘
src └─────────────┘ ┴ └─┘ └───────┘ └┘ ┴ └─┘ └───────┘ └┘ └─┘
typ └─────────────┘ ┴ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └─┘
doc └─────────────┘ └─┘ └───────┘ └─┘ └───────┘
153
154 attribute [irreducible] Hausdorff_edist
id └─────────────┘
src └─────────┘ └─────────────┘
typ └─────────────┘
doc └─────────┘ └─────────────┘
155
156 section Hausdorff_edist
157 open_locale ennreal
158 variables {α : Type u} {β : Type v} [emetric_space α] [emetric_space β]
id ┴ └───────────┘ └───────────┘
src └───────────┘ └───────────┘
typ ┴ └───────────┘ └───────────┘
doc └───────────┘ └───────────┘
159 {x y : α} {s t u : set α} {Φ : α → β}
id └─┘
src └─┘
typ └─┘
160
161 /-- The Hausdorff edistance of a set to itself vanishes -/
162 @[simp] lemma Hausdorff_edist_self : Hausdorff_edist s s = 0 :=
id └─────────────┘ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴
doc └──┘ └─────────────┘
163 begin
st └─────
164 erw [Hausdorff_edist_def, lattice.sup_idem, ← le_bot_iff],
id └─────────────────┘ └──────────────┘ └────────┘
src └───┘└─────────────────┘└┘└──────────────┘└──┘└────────┘┴
typ └───┘└─────────────────┘└┘└──────────────┘└──┘└────────┘┴
doc └───┘ └┘ └──┘ ┴
txt └───┘ └┘ └──┘ ┴
par └───┘ └┘ └──┘ ┴
pid └┘ └┘ └──┘ ┴
st ─────────────────────────┘└────────────────┘└────────────┘└──
165 apply Sup_le _,
id └────┘
src └────┘└────┘└┘
typ └────┘└────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ───────────────┘└─
166 simp [le_bot_iff, inf_edist_zero_of_mem] {contextual := tt},
id └────────┘ └───────────────────┘ └┘
src └────┘└────────┘└┘└───────────────────┘└┘ └────────────┘└┘┴
typ └────┘└────────┘└┘└───────────────────┘└┘ └────────────┘└┘┴
doc └────┘ └┘└───────────────────┘└┘ └────────────┘ ┴
txt └────┘ └┘ └┘ └────────────┘ ┴
par └────┘ └┘ └┘ └────────────┘ ┴
pid ┴┴ └┘ ┴┴ └────────────┘ ┴
st ────────────────────────────────────────────────────────────┘└─
167 end
st ──┘
168
169 /-- The Haudorff edistances of `s` to `t` and of `t` to `s` coincide -/
170 lemma Hausdorff_edist_comm : Hausdorff_edist s t = Hausdorff_edist t s :=
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
171 by unfold Hausdorff_edist; apply sup_comm
id └──────┘
src └────────────────────┘ └────┘└──────┘└
typ └────────────────────┘ └────┘└──────┘└
doc └────────────────────┘ └────┘ └
txt └────────────────────┘ └────┘ └
par └────────────────────┘ └────┘ └
pid └──────────────┘ ┴ └
st └───────────────────────────────────────
172
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
173 /-- Bounding the Hausdorff edistance by bounding the edistance of any point
174 in each set to the other set -/
175 lemma Hausdorff_edist_le_of_inf_edist {r : ennreal}
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
176 (H1 : ∀x ∈ s, inf_edist x t ≤ r) (H2 : ∀x ∈ t, inf_edist x s ≤ r) :
id ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴
typ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
177 Hausdorff_edist s t ≤ r :=
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
178 begin
st └─────
179 simp only [Hausdorff_edist, -mem_image, set.ball_image_iff, lattice.Sup_le_iff, lattice.sup_le_iff],
id └─────────────┘ └────────────────┘ └────────────────┘ └────────────────┘
src └─────────┘└─────────────┘└────────────┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
typ └─────────┘└─────────────┘└────────────┘└────────────────┘└┘└────────────────┘└┘└────────────────┘┴
doc └─────────┘└─────────────┘└────────────┘ └┘ └┘ ┴
txt └─────────┘ └────────────┘ └┘ └┘ ┴
par └─────────┘ └────────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └────────────┘ └┘ └┘ ┴
st ────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
180 exact ⟨H1, H2⟩
id └┘ └┘
src └────┘ └┘ └┘
typ └────┘ └┘└┘└┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴ └┘ ┴┴
st ────────────────┘
181 end
st └─┘
182
183 /-- Bounding the Hausdorff edistance by exhibiting, for any point in each set,
184 another point in the other set at controlled distance -/
185 lemma Hausdorff_edist_le_of_mem_edist {r : ennreal}
id └─────┘
src └─────┘
typ └─────┘
doc └─────┘
186 (H1 : ∀x ∈ s, ∃y ∈ t, edist x y ≤ r) (H2 : ∀x ∈ t, ∃y ∈ s, edist x y ≤ r) :
id ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴ ┴ ┴ └───┘ ┴
typ ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
187 Hausdorff_edist s t ≤ r :=
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
188 begin
st └─────
189 refine Hausdorff_edist_le_of_inf_edist _ _,
id └─────────────────────────────┘
src └─────┘└─────────────────────────────┘└──┘
typ └─────┘└─────────────────────────────┘└──┘
doc └─────┘└─────────────────────────────┘└──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────────────────────────┘└─
190 { assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
191 rcases H1 x xs with ⟨y, yt, hy⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ──────────────────────────────────┘└─
192 exact le_trans (inf_edist_le_edist_of_mem yt) hy },
id └──────┘ └───────────────────────┘ └┘ └┘
src └────┘└──────┘┴ └───────────────────────┘┴ └┘ ┴
typ └────┘└──────┘┴ └───────────────────────┘┴└┘└┘└┘┴
doc └────┘ ┴ └───────────────────────┘┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────┘└┘└
193 { assume x xt,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
194 rcases H2 x xt with ⟨y, ys, hy⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ──────────────────────────────────┘└─
195 exact le_trans (inf_edist_le_edist_of_mem ys) hy }
id └──────┘ └───────────────────────┘ └┘ └┘
src └────┘└──────┘┴ └───────────────────────┘┴ └┘ ┴
typ └────┘└──────┘┴ └───────────────────────┘┴└┘└┘└┘┴
doc └────┘ ┴ └───────────────────────┘┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ────────────────────────────────────────────────────┘└─
196 end
st ──┘
197
198 /-- The distance to a set is controlled by the Hausdorff distance -/
199 lemma inf_edist_le_Hausdorff_edist_of_mem (h : x ∈ s) : inf_edist x t ≤ Hausdorff_edist s t :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src ┴ └───────┘ ┴ └─────────────┘
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └───────┘ └─────────────┘
200 begin
st └─────
201 rw Hausdorff_edist_def,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
202 refine le_trans (le_Sup _) le_sup_left,
id └──────┘ └────┘ └─────────┘
src └─────┘└──────┘┴ └────┘└──┘└─────────┘
typ └─────┘└──────┘┴ └────┘└──┘└─────────┘
doc └─────┘ ┴ └──┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ───────────────────────────────────────┘└─
203 exact mem_image_of_mem _ h
id └──────────────┘ ┴
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘┴┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ────────────────────────────┘
204 end
st └─┘
205
206 /-- If the Hausdorff distance is `<r`, then any point in one of the sets has
207 a corresponding point at distance `<r` in the other set -/
208 lemma exists_edist_lt_of_Hausdorff_edist_lt {r : ennreal} (h : x ∈ s) (H : Hausdorff_edist s t < r) :
id └─────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src └─────┘ ┴ └─────────────┘ ┴
typ └─────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────────────┘
209 ∃y∈t, edist x y < r :=
id ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
src ┴ ┴ └───┘ ┴
typ ┴┴ ┴┴ └───┘ ┴ ┴ ┴ ┴
210 exists_edist_lt_of_inf_edist_lt $ calc
id └─────────────────────────────┘
src └─────────────────────────────┘
typ └─────────────────────────────┘
doc └─────────────────────────────┘
211 inf_edist x t ≤ Sup ((λx, inf_edist x t) '' s) : le_Sup (mem_image_of_mem _ h)
id └───────┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └────┘ └──────────────┘ ┴
src └───────┘ └─┘ └───────┘ └┘ └────┘ └──────────────┘
typ └───────┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └────┘ └──────────────┘ ┴
doc └───────┘ └─┘ └───────┘
212 ... ≤ Sup ((λx, inf_edist x t) '' s) ⊔ Sup ((λx, inf_edist x s) '' t) : le_sup_left
id └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └─────────┘
src └─┘ └───────┘ └┘ ┴ └─┘ └───────┘ └┘ └─────────┘
typ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ ┴ └─┘ ┴ └───────┘ ┴ ┴ └┘ ┴ └─────────┘
doc └─┘ └───────┘ └─┘ └───────┘
213 ... < r : by rwa Hausdorff_edist_def at H
id ┴ └─────────────────┘
src └──┘└─────────────────┘└─────
typ ┴ └──┘└─────────────────┘└─────
doc └──┘ └─────
txt └──┘ └─────
par └──┘ └─────
pid ┴ └───┘└
st └─────────────────────────────
214
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
215 /-- The distance from `x` to `s`or `t` is controlled in terms of the Hausdorff distance
216 between `s` and `t` -/
217 lemma inf_edist_le_inf_edist_add_Hausdorff_edist :
218 inf_edist x t ≤ inf_edist x s + Hausdorff_edist s t :=
id └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ └─────────────┘
typ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └───────┘ └───────┘ └─────────────┘
219 ennreal.le_of_forall_epsilon_le $ λε εpos h, begin
id └─────────────────────────────┘ ┴ └──┘ ┴
src └─────────────────────────────┘
typ └─────────────────────────────┘ ┴ └──┘ ┴
st └─────
220 have εpos' : (0 : ennreal) < ε := by simpa,
id └─────┘ ┴ ┴
src └───────────┘ └──┘└─────┘└┘┴┴ └──┘ ┴└───┘
typ └───────────┘ └──┘└─────┘└┘┴┴┴└──┘ ┴└───┘
doc └───────────┘ └──┘└─────┘└┘ ┴ └──┘ ┴└───┘
txt └───────────┘ └──┘ └┘ ┴ └──┘ ┴└───┘
par └───────────┘ └──┘ └┘ ┴ └──┘ ┴└───┘
pid └────────┘└─┘ └──┘ └┘ ┴ └──┘ └────┘
st ─────────────────────────────────────┘└────┘└─
221 have : inf_edist x s < inf_edist x s + ε/2 :=
id └───────┘ ┴ ┴ ┴ ┴┴
src └─────┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴┴┴ ┴└────
typ └─────┘ ┴ ┴ ┴ ┴└───────┘┴┴┴┴┴┴┴┴┴└────
doc └─────┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ └────
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
st ────────────────────────────────────────────────
222 ennreal.lt_add_right (ennreal.add_lt_top.1 h).1 (ennreal.half_pos εpos'),
id └──────────────────┘ └────────────────┘ ┴ └──────────────┘ └───┘
src ───┘└──────────────────┘┴ └────────────────┘└─┘ └──┘ └──────────────┘┴ ┴
typ ───┘└──────────────────┘┴ └────────────────┘└─┘┴└──┘ └──────────────┘┴└───┘┴
doc ───┘ ┴ └─┘ └──┘ ┴ ┴
txt ───┘ ┴ └─┘ └──┘ ┴ ┴
par ───┘ ┴ └─┘ └──┘ ┴ ┴
pid ───┘ ┴ └─┘ └──┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
223 rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ys, dxy⟩,
id └─────────────────────────────┘ └──┘
src └─────┘└─────────────────────────────┘┴ └────────────────┘
typ └─────┘└─────────────────────────────┘┴└──┘└────────────────┘
doc └─────┘└─────────────────────────────┘┴ └────────────────┘
txt └─────┘ ┴ └────────────────┘
par └─────┘ ┴ └────────────────┘
pid ┴ ┴ └────────────────┘
st ──────────────────────────────────────────────────────────────┘└─
224 -- y : α, ys : y ∈ s, dxy : edist x y < inf_edist x s + ↑ε / 2
st ───────────────────────────────────────────────────────────────────
225 have : Hausdorff_edist s t < Hausdorff_edist s t + ε/2 :=
id └─────────────┘ ┴ ┴ ┴
src └─────┘ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ ┴ ┴ └────
typ └─────┘ ┴ ┴ ┴ ┴└─────────────┘┴┴┴┴┴ ┴┴ └────
doc └─────┘ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ ┴ ┴ └────
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └────
st ────────────────────────────────────────────────────────────
226 ennreal.lt_add_right (ennreal.add_lt_top.1 h).2 (ennreal.half_pos εpos'),
id └──────────────────┘ └────────────────┘ ┴ └──────────────┘ └───┘
src ───┘└──────────────────┘┴ └────────────────┘└─┘ └──┘ └──────────────┘┴ ┴
typ ───┘└──────────────────┘┴ └────────────────┘└─┘┴└──┘ └──────────────┘┴└───┘┴
doc ───┘ ┴ └─┘ └──┘ ┴ ┴
txt ───┘ ┴ └─┘ └──┘ ┴ ┴
par ───┘ ┴ └─┘ └──┘ ┴ ┴
pid ───┘ ┴ └─┘ └──┘ ┴ ┴
st ───────────────────────────────────────────────────────────────────────────┘└─
227 rcases exists_edist_lt_of_Hausdorff_edist_lt ys this with ⟨z, zt, dyz⟩,
id └───────────────────────────────────┘ └┘ └──┘
src └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
typ └─────┘└───────────────────────────────────┘┴└┘┴└──┘└────────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └────────────────┘
txt └─────┘ ┴ ┴ └────────────────┘
par └─────┘ ┴ ┴ └────────────────┘
pid ┴ ┴ ┴ └────────────────┘
st ───────────────────────────────────────────────────────────────────────┘└─
228 -- z : α, zt : z ∈ t, dyz : edist y z < Hausdorff_edist s t + ↑ε / 2
st ─────────────────────────────────────────────────────────────────────────
229 calc inf_edist x t ≤ edist x z : inf_edist_le_edist_of_mem zt
id └──┘ └───┘ ┴ ┴ └───────────────────────┘ └┘
src └──┘ └───┘ └───────────────────────┘
typ └──┘ └───┘ ┴ ┴ └───────────────────────┘ └┘
doc └──┘ └───────────────────────┘
st ────────────────────────────────────────────────────────────────
230 ... ≤ edist x y + edist y z : edist_triangle _ _ _
id ┴ └────────────┘
src └────────────┘
typ ┴ └────────────┘
st ───────────────────────────────────────────────────────
231 ... ≤ (inf_edist x s + ε/2) + (Hausdorff_edist s t + ε/2) : add_le_add' (le_of_lt dxy) (le_of_lt dyz)
id └─────────┘ └─┘ └──────┘ └─┘
src └─────────┘ └──────┘
typ └─────────┘ └─┘ └──────┘ └─┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────────
232 ... = inf_edist x s + Hausdorff_edist s t + ε : by simp [ennreal.add_halves, add_comm]
id └───────┘ └─────────────┘ ┴ ┴ ┴ └────────────────┘ └──────┘
src └───────┘ └─────────────┘ └────┘└────────────────┘└┘└──────┘└┘
typ └───────┘ └─────────────┘ ┴ ┴ ┴ └────┘└────────────────┘└┘└──────┘└┘
doc └───────┘ └─────────────┘ └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ─────────────────────────────────────────────────────┘└───────────────────────────────────┘
233 end
st └─┘
234
235 /-- The Hausdorff edistance is invariant under eisometries -/
236 lemma Hausdorff_edist_image (h : isometry Φ) :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
237 Hausdorff_edist (Φ '' s) (Φ '' t) = Hausdorff_edist s t :=
id └─────────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └┘ └┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
238 begin
st └─────
239 unfold Hausdorff_edist,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ───────────────────────┘└─
240 congr,
src └───┘
typ └───┘
txt └───┘
par └───┘
st ──────┘└─
241 { ext b,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ───┘└───┘└─
242 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
243 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ─────┘└───────┘└─
244 rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
245 rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
246 rw [← hy', ← hz', inf_edist_image h],
id └─┘ └─┘ └─────────────┘ ┴
src └────┘ └──┘ └┘└─────────────┘┴ ┴
typ └────┘└─┘└──┘└─┘└┘└─────────────┘┴┴┴
doc └────┘ └──┘ └┘└─────────────┘┴ ┴
txt └────┘ └──┘ └┘ ┴ ┴
par └────┘ └──┘ └┘ ┴ ┴
pid └──┘ └──┘ └┘ ┴ ┴
st ──────────────┘└─────┘└─────────────────┘└──
247 exact mem_image_of_mem _ hz },
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────┘└┘└
248 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ──────────────┘└─
249 rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
250 rw [← hy', ← inf_edist_image h],
id └─┘ └─────────────┘ ┴
src └────┘ └──┘└─────────────┘┴ ┴
typ └────┘└─┘└──┘└─────────────┘┴┴┴
doc └────┘ └──┘└─────────────┘┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid └──┘ └──┘ ┴ ┴
st ──────────────┘└───────────────────┘└──
251 exact mem_image_of_mem _ (mem_image_of_mem _ hy) }},
id └──────────────┘ └┘
src └────┘ └─┘ └──────────────┘└─┘ └┘
typ └────┘ └─┘ └──────────────┘└─┘└┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ──────────────────────────────────────────────────────┘└─┘└
252 { ext b,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid └┘
st ────────┘└─
253 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
254 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ─────┘└───────┘└─
255 rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
256 rcases (mem_image _ _ _ ).1 hy with ⟨z, ⟨hz, hz'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
257 rw [← hy', ← hz', inf_edist_image h],
id └─┘ └─┘ └─────────────┘ ┴
src └────┘ └──┘ └┘└─────────────┘┴ ┴
typ └────┘└─┘└──┘└─┘└┘└─────────────┘┴┴┴
doc └────┘ └──┘ └┘└─────────────┘┴ ┴
txt └────┘ └──┘ └┘ ┴ ┴
par └────┘ └──┘ └┘ ┴ ┴
pid └──┘ └──┘ └┘ ┴ ┴
st ──────────────┘└─────┘└─────────────────┘└──
258 exact mem_image_of_mem _ hz },
id └──────────────┘ └┘
src └────┘└──────────────┘└─┘ ┴
typ └────┘└──────────────┘└─┘└┘┴
doc └────┘ └─┘ ┴
txt └────┘ └─┘ ┴
par └────┘ └─┘ ┴
pid ┴ └─┘ ┴
st ─────────────────────────────────┘└┘└
259 { assume hb,
src └───────┘
typ └───────┘
doc └───────┘
txt └───────┘
par └───────┘
pid └───────┘
st ──────────────┘└─
260 rcases (mem_image _ _ _ ).1 hb with ⟨y, ⟨hy, hy'⟩⟩,
id └───────┘ └┘
src └─────┘ └───────┘└─────────┘ └──────────────────┘
typ └─────┘ └───────┘└─────────┘└┘└──────────────────┘
doc └─────┘ └─────────┘ └──────────────────┘
txt └─────┘ └─────────┘ └──────────────────┘
par └─────┘ └─────────┘ └──────────────────┘
pid ┴ └─────────┘ └──────────────────┘
st ───────────────────────────────────────────────────────┘└─
261 rw [← hy', ← inf_edist_image h],
id └─┘ └─────────────┘ ┴
src └────┘ └──┘└─────────────┘┴ ┴
typ └────┘└─┘└──┘└─────────────┘┴┴┴
doc └────┘ └──┘└─────────────┘┴ ┴
txt └────┘ └──┘ ┴ ┴
par └────┘ └──┘ ┴ ┴
pid └──┘ └──┘ ┴ ┴
st ──────────────┘└───────────────────┘└──
262 exact mem_image_of_mem _ (mem_image_of_mem _ hy) }}
id └──────────────┘ └┘
src └────┘ └─┘ └──────────────┘└─┘ └┘
typ └────┘ └─┘ └──────────────┘└─┘└┘└┘
doc └────┘ └─┘ └─┘ └┘
txt └────┘ └─┘ └─┘ └┘
par └────┘ └─┘ └─┘ └┘
pid ┴ └─┘ └─┘ ┴┴
st ──────────────────────────────────────────────────────┘└──
263 end
st ──┘
264
265 /-- The Hausdorff distance is controlled by the diameter of the union -/
266 lemma Hausdorff_edist_le_ediam (hs : s.nonempty) (ht : t.nonempty) : Hausdorff_edist s t ≤ diam (s ∪ t) :=
id ┴└───────┘ ┴└───────┘ └─────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └───────┘ └───────┘ └─────────────┘ ┴ └──┘ ┴
typ ┴└───────┘ ┴└───────┘ └─────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └───────┘ └───────┘ └─────────────┘ └──┘
267 begin
st └─────
268 rcases hs with ⟨x, xs⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
269 rcases ht with ⟨y, yt⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
270 refine Hausdorff_edist_le_of_mem_edist _ _,
id └─────────────────────────────┘
src └─────┘└─────────────────────────────┘└──┘
typ └─────┘└─────────────────────────────┘└──┘
doc └─────┘└─────────────────────────────┘└──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────────────────────────┘└─
271 { exact λz hz, ⟨y, yt, edist_le_diam_of_mem (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩ },
id ┴ └──────────────────┘ └───────────────┘ └────────────────┘ └┘
src └────┘ └────┘ └┘ └┘└──────────────────┘┴ └───────────────┘└───┘ └┘ └────────────────┘└───┘ └─┘
typ └────┘ └────┘ ┴└┘ └┘└──────────────────┘┴ └───────────────┘└───┘ └┘ └────────────────┘└───┘└┘└─┘
doc └────┘ └────┘ └┘ └┘└──────────────────┘┴ └───┘ └┘ └───┘ └─┘
txt └────┘ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └─┘
par └────┘ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └─┘
pid ┴ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └┘┴
st ───┘└────────────────────────────────────────────────────────────────────────────────────────────────┘└┘└
272 { exact λz hz, ⟨x, xs, edist_le_diam_of_mem (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩ }
id ┴ └──────────────────┘ └────────────────┘ └───────────────┘ └┘
src └────┘ └────┘ └┘ └┘└──────────────────┘┴ └────────────────┘└───┘ └┘ └───────────────┘└───┘ └─┘
typ └────┘ └────┘ ┴└┘ └┘└──────────────────┘┴ └────────────────┘└───┘ └┘ └───────────────┘└───┘└┘└─┘
doc └────┘ └────┘ └┘ └┘└──────────────────┘┴ └───┘ └┘ └───┘ └─┘
txt └────┘ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └─┘
par └────┘ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └─┘
pid ┴ └────┘ └┘ └┘ ┴ └───┘ └┘ └───┘ └┘┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
273 end
st ──┘
274
275 /-- The Hausdorff distance satisfies the triangular inequality -/
276 lemma Hausdorff_edist_triangle : Hausdorff_edist s u ≤ Hausdorff_edist s t + Hausdorff_edist t u :=
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ ┴ └─────────────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘ └─────────────┘
277 begin
st └─────
278 rw Hausdorff_edist_def,
id └─────────────────┘
src └─┘└─────────────────┘
typ └─┘└─────────────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ───────────────────────┘└─
279 simp only [and_imp, set.mem_image, lattice.Sup_le_iff, exists_imp_distrib,
id └─────┘ └───────────┘ └────────────────┘ └────────────────┘
src └─────────┘└─────┘└┘└───────────┘└┘└────────────────┘└┘└────────────────┘└─
typ └─────────┘└─────┘└┘└───────────┘└┘└────────────────┘└┘└────────────────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └─
st ─────────────────────────────────────────────────────────────────────────────
280 lattice.sup_le_iff, -mem_image, set.ball_image_iff],
id └────────────────┘ └────────────────┘
src ────────────┘└────────────────┘└────────────┘└────────────────┘┴
typ ────────────┘└────────────────┘└────────────┘└────────────────┘┴
doc ────────────┘ └────────────┘ ┴
txt ────────────┘ └────────────┘ ┴
par ────────────┘ └────────────┘ ┴
pid ────────────┘ └────────────┘ ┴
st ───────────────────────────────────────────────────────────────┘└─
281 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ──────┘└─
282 show ∀x ∈ s, inf_edist x u ≤ Hausdorff_edist s t + Hausdorff_edist t u, from λx xs, calc
id └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └───┘ └──┘ ┴└───────┘┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴└─────────────┘┴ ┴ └───┘ └────┘ └
typ └───┘ └──┘ ┴└───────┘┴ ┴ ┴┴┴ ┴┴┴ ┴┴┴└─────────────┘┴┴┴┴ └───┘ └────┘ └
doc └───┘ └──┘ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └───┘ └────┘ └
txt └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
par └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
pid └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
st ───────────────────────────────────────────────────────────────────────────────────────────
283 inf_edist x u ≤ inf_edist x t + Hausdorff_edist t u : inf_edist_le_inf_edist_add_Hausdorff_edist
id └───────┘ └────────────────────────────────────────┘
src ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────────────────────────────┘└
typ ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────────────────────────────┘└
doc ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ └─┘└────────────────────────────────────────┘└
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
284 ... ≤ Hausdorff_edist s t + Hausdorff_edist t u :
id ┴ └─────────────┘ ┴ ┴
src ───────┘ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └──
typ ───────┘ ┴ ┴┴┴ ┴ ┴└─────────────┘┴┴┴┴└──
doc ───────┘ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └──
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────
285 add_le_add_right' (inf_edist_le_Hausdorff_edist_of_mem xs),
id └───────────────┘ └─────────────────────────────────┘
src ─────┘└───────────────┘┴ └─────────────────────────────────┘└┘ ┴
typ ─────┘└───────────────┘┴ └─────────────────────────────────┘└┘ ┴
doc ─────┘ ┴ └─────────────────────────────────┘└┘ ┴
txt ─────┘ ┴ └┘ ┴
par ─────┘ ┴ └┘ ┴
pid ─────┘ ┴ └┘ ┴
st ────────────────────────────────────────────────────────────────┘└─
286 show ∀x ∈ u, inf_edist x s ≤ Hausdorff_edist s t + Hausdorff_edist t u, from λx xu, calc
id └───────┘ ┴ └─────────────┘ ┴ ┴
src └───┘ └──┘ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └───┘ └────┘ └
typ └───┘ └──┘ ┴└───────┘┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└─────────────┘┴┴┴┴ └───┘ └────┘ └
doc └───┘ └──┘ ┴└───────┘┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └───┘ └────┘ └
txt └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
par └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
pid └───┘ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───┘ └────┘ └
st ───────────────────────────────────────────────────────────────────────────────────────────
287 inf_edist x s ≤ inf_edist x t + Hausdorff_edist t s : inf_edist_le_inf_edist_add_Hausdorff_edist
id └───────┘ └─────────────┘ ┴ ┴ └────────────────────────────────────────┘
src ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴└─────────────┘┴ ┴ └─┘└────────────────────────────────────────┘└
typ ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴└─────────────┘┴┴┴┴└─┘└────────────────────────────────────────┘└
doc ───┘ ┴ ┴ ┴ ┴└───────┘┴ ┴ ┴ ┴└─────────────┘┴ ┴ └─┘└────────────────────────────────────────┘└
txt ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────────────────
288 ... ≤ Hausdorff_edist u t + Hausdorff_edist t s :
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──
st ──────────────────────────────────────────────────────
289 add_le_add_right' (inf_edist_le_Hausdorff_edist_of_mem xu)
id └───────────────┘ └─────────────────────────────────┘
src ─────┘└───────────────┘┴ └─────────────────────────────────┘┴ └─
typ ─────┘└───────────────┘┴ └─────────────────────────────────┘┴ └─
doc ─────┘ ┴ └─────────────────────────────────┘┴ └─
txt ─────┘ ┴ ┴ └─
par ─────┘ ┴ ┴ └─
pid ─────┘ ┴ ┴ └─
st ─────────────────────────────────────────────────────────────────
290 ... = Hausdorff_edist s t + Hausdorff_edist t u : by simp [Hausdorff_edist_comm, add_comm]
id ┴ └──────────────────┘ └──────┘
src ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└──────────────────┘└┘└──────┘└┘
typ ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴└─┘ ┴└────┘└──────────────────┘└┘└──────┘└┘
doc ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└──────────────────┘└┘ └┘
txt ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘
par ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └┘ └┘
pid ───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────┘ └┘ └┘
st ───────────────────────────────────────────────────────┘└─────────────────────────────────────┘
291 end
st └─┘
292
293 /-- The Hausdorff edistance between a set and its closure vanishes -/
294 @[simp] lemma Hausdorff_edist_self_closure : Hausdorff_edist s (closure s) = 0 :=
id └─────────────┘ ┴ └─────┘ ┴ ┴
src └─────────────┘ └─────┘ ┴
typ └─────────────┘ ┴ └─────┘ ┴ ┴
doc └──┘ └─────────────┘ └─────┘
295 begin
st └─────
296 erw ← le_bot_iff,
id └────────┘
src └────┘└────────┘
typ └────┘└────────┘
doc └────┘
txt └────┘
par └────┘
pid └─┘
st ─────────────────┘└─
297 simp only [Hausdorff_edist, inf_edist_closure, -le_zero_iff_eq, and_imp,
id └─────────────┘ └───────────────┘ └─────┘
src └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘└─────┘└─
typ └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘└─────┘└─
doc └─────────┘└─────────────┘└┘└───────────────┘└─────────────────┘ └─
txt └─────────┘ └┘ └─────────────────┘ └─
par └─────────┘ └┘ └─────────────────┘ └─
pid ┴└──┘└┘ └┘ └─────────────────┘ └─
st ───────────────────────────────────────────────────────────────────────────
298 set.mem_image, lattice.Sup_le_iff, exists_imp_distrib, lattice.sup_le_iff,
id └───────────┘ └────────────────┘ └────────────────┘ └────────────────┘
src ───┘└───────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────────┘└─
typ ───┘└───────────┘└┘└────────────────┘└┘└────────────────┘└┘└────────────────┘└─
doc ───┘ └┘ └┘ └┘ └─
txt ───┘ └┘ └┘ └┘ └─
par ───┘ └┘ └┘ └┘ └─
pid ───┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────────
299 set.ball_image_iff, ennreal.bot_eq_zero, -mem_image],
id └────────────────┘ └─────────────────┘
src ───┘└────────────────┘└┘└─────────────────┘└───────────┘
typ ───┘└────────────────┘└┘└─────────────────┘└───────────┘
doc ───┘ └┘ └───────────┘
txt ───┘ └┘ └───────────┘
par ───┘ └┘ └───────────┘
pid ───┘ └┘ └───────────┘
st ───────────────────────────────────────────────────────┘└─
300 simp only [inf_edist_zero_of_mem, mem_closure_iff_inf_edist_zero, le_refl, and_self,
id └───────────────────┘ └────────────────────────────┘ └─────┘ └──────┘
src └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘└─────┘└┘└──────┘└─
typ └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘└─────┘└┘└──────┘└─
doc └─────────┘└───────────────────┘└┘└────────────────────────────┘└┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────────────────
301 forall_true_iff] {contextual := tt}
id └─────────────┘ └┘
src ────────────┘└─────────────┘└┘ └────────────┘└┘└┘
typ ────────────┘└─────────────┘└┘ └────────────┘└┘└┘
doc ────────────┘ └┘ └────────────┘ └┘
txt ────────────┘ └┘ └────────────┘ └┘
par ────────────┘ └┘ └────────────┘ └┘
pid ────────────┘ ┴┴ └────────────┘ ┴┴
st ────────────────────────────────────────────────┘
302 end
st └─┘
303
304 /-- Replacing a set by its closure does not change the Hausdorff edistance. -/
305 @[simp] lemma Hausdorff_edist_closure₁ : Hausdorff_edist (closure s) t = Hausdorff_edist s t :=
id └─────────────┘ └─────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────┘ ┴ └─────────────┘
typ └─────────────┘ └─────┘ ┴ ┴ ┴ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘ └─────┘ └─────────────┘
306 begin
st └─────
307 refine le_antisymm _ _,
id └─────────┘
src └─────┘└─────────┘└──┘
typ └─────┘└─────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────┘└─
308 { calc _ ≤ Hausdorff_edist (closure s) s + Hausdorff_edist s t : Hausdorff_edist_triangle
id └──┘ └─────┘ ┴ └──────────────────────┘
src └──┘ └─────┘ ┴ └──────────────────────┘
typ └──┘ └─────┘ ┴ └──────────────────────┘
doc └──┘ └─────┘ └──────────────────────┘
st ───┘└────────────────────────────────────────────────────────────────────────────────────────
309 ... = Hausdorff_edist s t : by simp [Hausdorff_edist_comm] },
id └─────────────┘ ┴ ┴ └──────────────────┘
src └─────────────┘ └────┘└──────────────────┘└┘
typ └─────────────┘ ┴ ┴ └────┘└──────────────────┘└┘
doc └─────────────┘ └────┘└──────────────────┘└┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ─────────────────────────────────┘└───────────────────────────┘└┘└
310 { calc _ ≤ Hausdorff_edist s (closure s) + Hausdorff_edist (closure s) t : Hausdorff_edist_triangle
id └──┘ └──────────────────────┘
src └──┘ └──────────────────────┘
typ └──┘ └──────────────────────┘
doc └──┘ └──────────────────────┘
st ──────────────────────────────────────────────────────────────────────────────────────────────────────
311 ... = Hausdorff_edist (closure s) t : by simp }
id └─────────────┘ └─────┘ ┴ ┴
src └─────────────┘ └─────┘ └───┘
typ └─────────────┘ └─────┘ ┴ ┴ └───┘
doc └─────────────┘ └─────┘ └───┘
txt └───┘
par └───┘
pid ┴
st ───────────────────────────────────────────┘└────┘└─
312 end
st ──┘
313
314 /-- Replacing a set by its closure does not change the Hausdorff edistance. -/
315 @[simp] lemma Hausdorff_edist_closure₂ : Hausdorff_edist s (closure t) = Hausdorff_edist s t :=
id └─────────────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────┘ ┴ └─────────────┘
typ └─────────────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘ └─────┘ └─────────────┘
316 by simp [@Hausdorff_edist_comm _ _ s _]
id └──────────────────┘ ┴
src └────┘ └──────────────────┘└───┘ └───
typ └────┘ └──────────────────┘└───┘┴└───
doc └────┘ └──────────────────┘└───┘ └───
txt └────┘ └───┘ └───
par └────┘ └───┘ └───
pid ┴┴ └───┘ └─┘└
st └─────────────────────────────────────
317
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
318 /-- The Hausdorff edistance between sets or their closures is the same -/
319 @[simp] lemma Hausdorff_edist_closure : Hausdorff_edist (closure s) (closure t) = Hausdorff_edist s t :=
id └─────────────┘ └─────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴
src └─────────────┘ └─────┘ └─────┘ ┴ └─────────────┘
typ └─────────────┘ └─────┘ ┴ └─────┘ ┴ ┴ └─────────────┘ ┴ ┴
doc └──┘ └─────────────┘ └─────┘ └─────┘ └─────────────┘
320 by simp
src └────
typ └────
doc └────
txt └────
par └────
pid └
st └─────
321
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
322 /-- Two sets are at zero Hausdorff edistance if and only if they have the same closure -/
323 lemma Hausdorff_edist_zero_iff_closure_eq_closure : Hausdorff_edist s t = 0 ↔ closure s = closure t :=
id └─────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └─────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └─────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └─────────────┘ └─────┘ └─────┘
324 ⟨begin
st └─────
325 assume h,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └──────┘
st ─────────┘└─
326 refine subset.antisymm _ _,
id └─────────────┘
src └─────┘└─────────────┘└──┘
typ └─────┘└─────────────┘└──┘
doc └─────┘ └──┘
txt └─────┘ └──┘
par └─────┘ └──┘
pid ┴ └──┘
st ───────────────────────────┘└─
327 { have : s ⊆ closure t := λx xs, mem_closure_iff_inf_edist_zero.2 $ begin
id ┴ ┴ └─────┘ ┴ └────────────────────────────┘
src └─────┘ ┴┴┴└─────┘┴ └──┘ └────┘└────────────────────────────┘└─┘ ┴ └
typ └─────┘┴┴┴┴└─────┘┴┴└──┘ └────┘└────────────────────────────┘└─┘ ┴ └
doc └─────┘ ┴ ┴└─────┘┴ └──┘ └────┘└────────────────────────────┘└─┘ ┴ └
txt └─────┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
par └─────┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
pid └───┘└┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
st ───┘└────────────────────────────────────────────────────────────────┘└─────
328 erw ← le_bot_iff,
id └────────┘
src ─────┘└────┘└────────┘└─
typ ─────┘└────┘└────────┘└─
doc ─────┘└────┘ └─
txt ─────┘└────┘ └─
par ─────┘└────┘ └─
pid ───────────┘ └─
st ─────────────────────┘└─
329 have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ t xs,
id └─────────────────────────────────┘ ┴ └┘
src ─────────────┘ └─────────────────────────────────┘└───────┘ ┴ └─
typ ─────────────┘ └─────────────────────────────────┘└───────┘┴┴└┘└─
doc ─────────────┘ └─────────────────────────────────┘└───────┘ ┴ └─
txt ─────────────┘ └───────┘ ┴ └─
par ─────────────┘ └───────┘ ┴ └─
pid ─────────────┘ └───────┘ ┴ └─
st ──────────────────────────────────────────────────────────────┘└─
330 rwa h at this,
id ┴
src ─────┘└──┘ └──────┘└─
typ ─────┘└──┘┴└──────┘└─
doc ─────┘└──┘ └──────┘└─
txt ─────┘└──┘ └──────┘└─
par ─────┘└──┘ └──────┘└─
pid ─────────┘ └─────────
st ──────────────────┘└─
331 end,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘
332 by rw ← @closure_closure _ _ t; exact closure_mono this },
id └─────────────┘ ┴ └──────────┘ └──┘
src └───┘ └─────────────┘└───┘ └────┘└──────────┘┴ ┴
typ └───┘ └─────────────┘└───┘┴ └────┘└──────────┘┴└──┘┴
doc └───┘ └───┘ └────┘ ┴ ┴
txt └───┘ └───┘ └────┘ ┴ ┴
par └───┘ └───┘ └────┘ ┴ ┴
pid └─┘ └───┘ ┴ ┴ ┴
st └┘└
333 { have : t ⊆ closure s := λx xt, mem_closure_iff_inf_edist_zero.2 $ begin
id ┴ └─────┘ ┴ └────────────────────────────┘
src └─────┘ ┴ ┴└─────┘┴ └──┘ └────┘└────────────────────────────┘└─┘ ┴ └
typ └─────┘┴┴ ┴└─────┘┴┴└──┘ └────┘└────────────────────────────┘└─┘ ┴ └
doc └─────┘ ┴ ┴└─────┘┴ └──┘ └────┘└────────────────────────────┘└─┘ ┴ └
txt └─────┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
par └─────┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
pid └───┘└┘ ┴ ┴ ┴ └──┘ └────┘ └─┘ ┴ └
st ─────────────────────────────────────────────────────────────────────┘└─────
334 erw ← le_bot_iff,
id └────────┘
src ─────┘└────┘└────────┘└─
typ ─────┘└────┘└────────┘└─
doc ─────┘└────┘ └─
txt ─────┘└────┘ └─
par ─────┘└────┘ └─
pid ───────────┘ └─
st ─────────────────────┘└─
335 have := @inf_edist_le_Hausdorff_edist_of_mem _ _ _ _ s xt,
id └─────────────────────────────────┘ ┴ └┘
src ─────────────┘ └─────────────────────────────────┘└───────┘ ┴ └─
typ ─────────────┘ └─────────────────────────────────┘└───────┘┴┴└┘└─
doc ─────────────┘ └─────────────────────────────────┘└───────┘ ┴ └─
txt ─────────────┘ └───────┘ ┴ └─
par ─────────────┘ └───────┘ ┴ └─
pid ─────────────┘ └───────┘ ┴ └─
st ──────────────────────────────────────────────────────────────┘└─
336 rw Hausdorff_edist_comm at h,
id └──────────────────┘
src ─────┘└─┘└──────────────────┘└───┘└─
typ ─────┘└─┘└──────────────────┘└───┘└─
doc ─────┘└─┘└──────────────────┘└───┘└─
txt ─────┘└─┘ └───┘└─
par ─────┘└─┘ └───┘└─
pid ────────┘ └──────
st ─────────────────────────────────┘└─
337 rwa h at this,
id ┴
src ─────┘└──┘ └──────┘└─
typ ─────┘└──┘┴└──────┘└─
doc ─────┘└──┘ └──────┘└─
txt ─────┘└──┘ └──────┘└─
par ─────┘└──┘ └──────┘└─
pid ─────────┘ └─────────
st ──────────────────┘└─
338 end,
src ──────┘
typ ──────┘
doc ──────┘
txt ──────┘
par ──────┘
pid ──────┘
st ──────┘
339 by rw ← @closure_closure _ _ s; exact closure_mono this }
id └─────────────┘ ┴ └──────────┘ └──┘
src └───┘ └─────────────┘└───┘ └────┘└──────────┘┴ ┴
typ └───┘ └─────────────┘└───┘┴ └────┘└──────────┘┴└──┘┴
doc └───┘ └───┘ └────┘ ┴ ┴
txt └───┘ └───┘ └────┘ ┴ ┴
par └───┘ └───┘ └────┘ ┴ ┴
pid └─┘ └───┘ ┴ ┴ ┴
st └─
340 end,
st ──┘
341 λh, by rw [← Hausdorff_edist_closure, h, Hausdorff_edist_self]⟩
id ┴ └─────────────────────┘ ┴ └──────────────────┘
src └────┘└─────────────────────┘└┘ └┘└──────────────────┘┴
typ ┴ └────┘└─────────────────────┘└┘┴└┘└──────────────────┘┴
doc └────┘└─────────────────────┘└┘ └┘└──────────────────┘┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st └────────────────────────────┘└─┘└────────────────────┘┴
342
343 /-- Two closed sets are at zero Hausdorff edistance if and only if they coincide -/
344 lemma Hausdorff_edist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t) :
id └───────┘ ┴ └───────┘ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ └───────┘ ┴
doc └───────┘ └───────┘
345 Hausdorff_edist s t = 0 ↔ s = t :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘
346 by rw [Hausdorff_edist_zero_iff_closure_eq_closure, closure_eq_iff_is_closed.2 hs,
id └─────────────────────────────────────────┘ └──────────────────────┘ └┘
src └──┘└─────────────────────────────────────────┘└┘└──────────────────────┘└─┘ └─
typ └──┘└─────────────────────────────────────────┘└┘└──────────────────────┘└─┘└┘└─
doc └──┘└─────────────────────────────────────────┘└┘ └─┘ └─
txt └──┘ └┘ └─┘ └─
par └──┘ └┘ └─┘ └─
pid └┘ └┘ └─┘ └─
st └──────────────────────────────────────────────┘└─────────────────────────────┘└─
347 closure_eq_iff_is_closed.2 ht]
id └──────────────────────┘ └┘
src ──────┘└──────────────────────┘└─┘ └─
typ ──────┘└──────────────────────┘└─┘└┘└─
doc ──────┘ └─┘ └─
txt ──────┘ └─┘ └─
par ──────┘ └─┘ └─
pid ──────┘ └─┘ ┴└
st ───────────────────────────────────┘┴└
348
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
349 /-- The Haudorff edistance to the empty set is infinite -/
350 lemma Hausdorff_edist_empty (ne : s.nonempty) : Hausdorff_edist s ∅ = ∞ :=
id ┴└───────┘ └─────────────┘ ┴ ┴ ┴ ┴
src └───────┘ └─────────────┘ ┴ ┴ ┴
typ ┴└───────┘ └─────────────┘ ┴ ┴ ┴ ┴
doc └───────┘ └─────────────┘ ┴
351 begin
st └─────
352 rcases ne with ⟨x, xs⟩,
id └┘
src └─────┘└┘└───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
353 have : inf_edist x ∅ ≤ Hausdorff_edist s ∅ := inf_edist_le_Hausdorff_edist_of_mem xs,
id └───────┘ ┴ ┴ ┴ └─────────────┘ ┴ └─────────────────────────────────┘ └┘
src └─────┘└───────┘┴ ┴┴┴┴┴└─────────────┘┴ ┴ └──┘└─────────────────────────────────┘┴
typ └─────┘└───────┘┴┴┴┴┴┴┴└─────────────┘┴┴┴ └──┘└─────────────────────────────────┘┴└┘
doc └─────┘└───────┘┴ ┴ ┴ ┴└─────────────┘┴ ┴ └──┘└─────────────────────────────────┘┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────┘└─
354 simpa using this,
id └──┘
src └──────────┘
typ └──────────┘└──┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴└────┘
st ─────────────────┘└─
355 end
st ──┘
356
357 /-- If a set is at finite Hausdorff edistance of a nonempty set, it is nonempty -/
358 lemma nonempty_of_Hausdorff_edist_ne_top (hs : s.nonempty) (fin : Hausdorff_edist s t ≠ ⊤) :
id ┴└───────┘ └─────────────┘ ┴ ┴ ┴ ┴
src └───────┘ └─────────────┘ ┴ ┴
typ ┴└───────┘ └─────────────┘ ┴ ┴ ┴ ┴
doc └───────┘ └─────────────┘
359 t.nonempty :=
id ┴└───────┘
src └───────┘
typ ┴└───────┘
doc └───────┘
360 t.eq_empty_or_nonempty.elim (λ ht, (fin $ ht.symm ▸ Hausdorff_edist_empty hs).elim) id
id ┴└───────────────────┘└───┘ └┘ └─┘ └┘└───┘ ┴ └───────────────────┘ └┘ └──┘ └┘
src └───────────────────┘└───┘ └─┘ └───┘ ┴ └───────────────────┘ └──┘ └┘
typ ┴└───────────────────┘└───┘ └┘ └─┘ └┘└───┘ ┴ └───────────────────┘ └┘ └──┘ └┘
doc └───────────────────┘
361
362 lemma empty_or_nonempty_of_Hausdorff_edist_ne_top (fin : Hausdorff_edist s t ≠ ⊤) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
363 s = ∅ ∧ t = ∅ ∨ s.nonempty ∧ t.nonempty :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴└───────┘
src ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘
364 begin
st └─────
365 cases s.eq_empty_or_nonempty with hs hs,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘└─
366 { cases t.eq_empty_or_nonempty with ht ht,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ───┘└─────────────────────────────────────┘└─
367 { exact or.inl ⟨hs, ht⟩ },
id └────┘ └┘ └┘
src └────┘└────┘┴ └┘ └┘
typ └────┘└────┘┴ └┘└┘└┘└┘
doc └────┘ ┴ └┘ └┘
txt └────┘ ┴ └┘ └┘
par └────┘ ┴ └┘ └┘
pid ┴ ┴ └┘ ┴┴
st ─────┘└────────────────────┘└┘└
368 { rw Hausdorff_edist_comm at fin,
id └──────────────────┘
src └─┘└──────────────────┘└─────┘
typ └─┘└──────────────────┘└─────┘
doc └─┘└──────────────────┘└─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────────────┘└─
369 exact or.inr ⟨nonempty_of_Hausdorff_edist_ne_top ht fin, ht⟩ } },
id └────┘ └────────────────────────────────┘ └─┘ └┘
src └────┘└────┘┴ └────────────────────────────────┘┴ ┴└─┘└┘ └┘
typ └────┘└────┘┴ └────────────────────────────────┘┴ ┴└─┘└┘└┘└┘
doc └────┘ ┴ └────────────────────────────────┘┴ ┴ └┘ └┘
txt └────┘ ┴ ┴ ┴ └┘ └┘
par └────┘ ┴ ┴ ┴ └┘ └┘
pid ┴ ┴ ┴ ┴ └┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘└──┘└
370 { exact or.inr ⟨hs, nonempty_of_Hausdorff_edist_ne_top hs fin⟩ }
id └────┘ └────────────────────────────────┘ └┘ └─┘
src └────┘└────┘┴ └┘└────────────────────────────────┘┴ ┴└─┘└┘
typ └────┘└────┘┴ └┘└────────────────────────────────┘┴└┘┴└─┘└┘
doc └────┘ ┴ └┘└────────────────────────────────┘┴ ┴ └┘
txt └────┘ ┴ └┘ ┴ ┴ └┘
par └────┘ ┴ └┘ ┴ ┴ └┘
pid ┴ ┴ └┘ ┴ ┴ ┴┴
st ────────────────────────────────────────────────────────────────┘└─
371 end
st ──┘
372
373 end Hausdorff_edist -- section
374 end emetric --namespace
375
376
377 /-Now, we turn to the same notions in metric spaces. To avoid the difficulties related to
378 Inf and Sup on ℝ (which is only conditionnally complete), we use the notions in ennreal formulated
379 in terms of the edistance, and coerce them to ℝ. Then their properties follow readily from the
380 corresponding properties in ennreal, modulo some tedious rewriting of inequalities from one to the
381 other -/
382
383 namespace metric
384 section
385 variables {α : Type u} {β : Type v} [metric_space α] [metric_space β] {s t u : set α} {x y : α} {Φ : α → β}
id ┴ └──────────┘ └──────────┘ └─┘
src └──────────┘ └──────────┘ └─┘
typ ┴ └──────────┘ └──────────┘ └─┘
doc └──────────┘ └──────────┘
386 open emetric
387
388 /-- The minimal distance of a point to a set -/
389 def inf_dist (x : α) (s : set α) : ℝ := ennreal.to_real (inf_edist x s)
id ┴ └─┘ ┴ ┴ └─────────────┘ └───────┘ ┴ ┴
src └─┘ ┴ └─────────────┘ └───────┘
typ ┴ └─┘ ┴ ┴ └─────────────┘ └───────┘ ┴ ┴
doc └─────────────┘ └───────┘
390
391 /-- the minimal distance is always nonnegative -/
392 lemma inf_dist_nonneg : 0 ≤ inf_dist x s := by simp [inf_dist]
id ┴ └──────┘ ┴ ┴ └──────┘
src ┴ └──────┘ └────┘└──────┘└─
typ ┴ └──────┘ ┴ ┴ └────┘└──────┘└─
doc └──────┘ └────┘└──────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
393
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
394 /-- the minimal distance to the empty set is 0 (if you want to have the more reasonable
395 value ∞ instead, use `inf_edist`, which takes values in ennreal) -/
396 @[simp] lemma inf_dist_empty : inf_dist x ∅ = 0 :=
id └──────┘ ┴ ┴ ┴
src └──────┘ ┴ ┴
typ └──────┘ ┴ ┴ ┴
doc └──┘ └──────┘
397 by simp [inf_dist]
id └──────┘
src └────┘└──────┘└─
typ └────┘└──────┘└─
doc └────┘└──────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────
398
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
399 /-- In a metric space, the minimal edistance to a nonempty set is finite -/
400 lemma inf_edist_ne_top (h : s.nonempty) : inf_edist x s ≠ ⊤ :=
id ┴└───────┘ └───────┘ ┴ ┴ ┴ ┴
src └───────┘ └───────┘ ┴ ┴
typ ┴└───────┘ └───────┘ ┴ ┴ ┴ ┴
doc └───────┘ └───────┘
401 begin
st └─────
402 rcases h with ⟨y, hy⟩,
id ┴
src └─────┘ └───────────┘
typ └─────┘┴└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ──────────────────────┘└─
403 apply lt_top_iff_ne_top.1,
id └───────────────┘
src └────┘└───────────────┘└┘
typ └────┘└───────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴ └┘
st ──────────────────────────┘└─
404 calc inf_edist x s ≤ edist x y : inf_edist_le_edist_of_mem hy
id └──┘ └───────┘ ┴ └───┘ ┴ ┴ └───────────────────────┘ └┘
src └──┘ └───────┘ └───┘ └───────────────────────┘
typ └──┘ └───────┘ ┴ └───┘ ┴ ┴ └───────────────────────┘ └┘
doc └──┘ └───────┘ └───────────────────────┘
st ────────────────────────────────────────────────────────────────
405 ... < ⊤ : lt_top_iff_ne_top.2 (edist_ne_top _ _)
id ┴ └───────────────┘┴ └──────────┘
src ┴ └───────────────┘┴ └──────────┘
typ ┴ └───────────────┘┴ └──────────┘
doc └──────────┘
st ──────────────────────────────────────────────────────┘└
406 end
st ──┘
407
408 /-- The minimal distance of a point to a set containing it vanishes -/
409 lemma inf_dist_zero_of_mem (h : x ∈ s) : inf_dist x s = 0 :=
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src ┴ └──────┘ ┴
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
410 by simp [inf_edist_zero_of_mem h, inf_dist]
id └───────────────────┘ ┴ └──────┘
src └────┘└───────────────────┘┴ └┘└──────┘└─
typ └────┘└───────────────────┘┴┴└┘└──────┘└─
doc └────┘└───────────────────┘┴ └┘└──────┘└─
txt └────┘ ┴ └┘ └─
par └────┘ ┴ └┘ └─
pid ┴┴ ┴ └┘ ┴└
st └─────────────────────────────────────────
411
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
412 /-- The minimal distance to a singleton is the distance to the unique point in this singleton -/
413 @[simp] lemma inf_dist_singleton : inf_dist x {y} = dist x y :=
id └──────┘ ┴ ┴┴ ┴ └──┘ ┴ ┴
src └──────┘ ┴ ┴ └──┘
typ └──────┘ ┴ ┴┴ ┴ └──┘ ┴ ┴
doc └──┘ └──────┘
414 by simp [inf_dist, inf_edist, dist_edist]
id └──────┘ └───────┘ └────────┘
src └────┘└──────┘└┘└───────┘└┘└────────┘└─
typ └────┘└──────┘└┘└───────┘└┘└────────┘└─
doc └────┘└──────┘└┘└───────┘└┘└────────┘└─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └───────────────────────────────────────
415
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
416 /-- The minimal distance to a set is bounded by the distance to any point in this set -/
417 lemma inf_dist_le_dist_of_mem (h : y ∈ s) : inf_dist x s ≤ dist x y :=
id ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src ┴ └──────┘ ┴ └──┘
typ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──────┘
418 begin
st └─────
419 rw [dist_edist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ⟨_, h⟩) (edist_ne_top _ _)],
id └────────┘ └──────┘ └────────────────────────┘ └──────────────┘ ┴ └──────────┘
src └──┘└────────┘└┘└──────┘└┘└────────────────────────┘┴ └──────────────┘┴ └─┘ └─┘ └──────────┘└────┘
typ └──┘└────────┘└┘└──────┘└┘└────────────────────────┘┴ └──────────────┘┴ └─┘┴└─┘ └──────────┘└────┘
doc └──┘└────────┘└┘└──────┘└┘ ┴ └──────────────┘┴ └─┘ └─┘ └──────────┘└────┘
txt └──┘ └┘ └┘ ┴ ┴ └─┘ └─┘ └────┘
par └──┘ └┘ └┘ ┴ ┴ └─┘ └─┘ └────┘
pid └┘ └┘ └┘ ┴ ┴ └─┘ └─┘ └────┘
st ───────────────┘└────────┘└───────────────────────────────────────────────────────────────────────┘└──
420 exact inf_edist_le_edist_of_mem h
id └───────────────────────┘ ┴
src └────┘└───────────────────────┘┴ ┴
typ └────┘└───────────────────────┘┴┴┴
doc └────┘└───────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ───────────────────────────────────┘
421 end
st └─┘
422
423 /-- The minimal distance is monotonous with respect to inclusion -/
424 lemma inf_dist_le_inf_dist_of_subset (h : s ⊆ t) (hs : s.nonempty) :
id ┴ ┴ ┴ ┴└───────┘
src ┴ └───────┘
typ ┴ ┴ ┴ ┴└───────┘
doc └───────┘
425 inf_dist x t ≤ inf_dist x s :=
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
426 begin
st └─────
427 have ht : t.nonempty := hs.mono h,
id └────────┘ └─────┘ ┴
src └────────┘└────────┘└──┘└─────┘┴
typ └────────┘└────────┘└──┘└─────┘┴┴
doc └────────┘└────────┘└──┘ ┴
txt └────────┘ └──┘ ┴
par └────────┘ └──┘ ┴
pid └─────┘└─┘ └──┘ ┴
st ──────────────────────────────────┘└─
428 rw [inf_dist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ht) (inf_edist_ne_top hs)],
id └──────┘ └──────┘ └────────────────────────┘ └┘ └──────────────┘ └┘
src └──┘└──────┘└┘└──────┘└┘└────────────────────────┘┴ ┴ └┘ └──────────────┘┴ └┘
typ └──┘└──────┘└┘└──────┘└┘└────────────────────────┘┴ ┴└┘└┘ └──────────────┘┴└┘└┘
doc └──┘└──────┘└┘└──────┘└┘ ┴ ┴ └┘ └──────────────┘┴ └┘
txt └──┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘
par └──┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘
pid └┘ └┘ └┘ ┴ ┴ └┘ ┴ └┘
st ─────────────┘└────────┘└──────────────────────────────────────────────────────────────────────┘└──
429 exact inf_edist_le_inf_edist_of_subset h
id └──────────────────────────────┘ ┴
src └────┘└──────────────────────────────┘┴ ┴
typ └────┘└──────────────────────────────┘┴┴┴
doc └────┘└──────────────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────┘
430 end
st └─┘
431
432 /-- If the minimal distance to a set is `<r`, there exists a point in this set at distance `<r` -/
433 lemma exists_dist_lt_of_inf_dist_lt {r : real} (h : inf_dist x s < r) (hs : s.nonempty) :
id └──┘ └──────┘ ┴ ┴ ┴ ┴ ┴└───────┘
src └──┘ └──────┘ ┴ └───────┘
typ └──┘ └──────┘ ┴ ┴ ┴ ┴ ┴└───────┘
doc └──────┘ └───────┘
434 ∃y∈s, dist x y < r :=
id ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴
typ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
435 begin
st └─────
436 have rpos : 0 < r := lt_of_le_of_lt inf_dist_nonneg h,
id ┴ ┴ └────────────┘ └─────────────┘ ┴
src └────────────┘┴┴ └──┘└────────────┘┴└─────────────┘┴
typ └────────────┘┴┴┴└──┘└────────────┘┴└─────────────┘┴┴
doc └────────────┘ ┴ └──┘ ┴└─────────────┘┴
txt └────────────┘ ┴ └──┘ ┴ ┴
par └────────────┘ ┴ └──┘ ┴ ┴
pid └───────┘└───┘ ┴ └──┘ ┴ ┴
st ──────────────────────────────────────────────────────┘└─
437 have : inf_edist x s < ennreal.of_real r,
id └───────┘ ┴ ┴ └─────────────┘ ┴
src └─────┘└───────┘┴ ┴ ┴ ┴└─────────────┘┴
typ └─────┘└───────┘┴┴┴┴┴ ┴└─────────────┘┴┴
doc └─────┘└───────┘┴ ┴ ┴ ┴└─────────────┘┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────┘└─
438 { rwa [inf_dist, ← ennreal.to_real_of_real (le_of_lt rpos), ennreal.to_real_lt_to_real (inf_edist_ne_top hs)] at h,
id └──────┘ └─────────────────────┘ └──────┘ └──┘ └────────────────────────┘ └──────────────┘ └┘
src └───┘└──────┘└──┘└─────────────────────┘┴ └──────┘┴ └─┘└────────────────────────┘┴ └──────────────┘┴ └─────┘
typ └───┘└──────┘└──┘└─────────────────────┘┴ └──────┘┴└──┘└─┘└────────────────────────┘┴ └──────────────┘┴└┘└─────┘
doc └───┘└──────┘└──┘ ┴ ┴ └─┘ ┴ └──────────────┘┴ └─────┘
txt └───┘ └──┘ ┴ ┴ └─┘ ┴ ┴ └─────┘
par └───┘ └──┘ ┴ ┴ └─┘ ┴ ┴ └─────┘
pid └┘ └──┘ ┴ ┴ └─┘ ┴ ┴ └┘└───┘
st ───┘└───────────┘└─────────────────────────────────────────┘└────────────────────────────────────────────────┘┴└───┘└─
439 simp },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ────────┘└┘└
440 rcases exists_edist_lt_of_inf_edist_lt this with ⟨y, ys, hy⟩,
id └─────────────────────────────┘ └──┘
src └─────┘└─────────────────────────────┘┴ └───────────────┘
typ └─────┘└─────────────────────────────┘┴└──┘└───────────────┘
doc └─────┘└─────────────────────────────┘┴ └───────────────┘
txt └─────┘ ┴ └───────────────┘
par └─────┘ ┴ └───────────────┘
pid ┴ ┴ └───────────────┘
st ─────────────────────────────────────────────────────────────┘└─
441 rw [edist_dist, ennreal.of_real_lt_of_real_iff rpos] at hy,
id └────────┘ └────────────────────────────┘ └──┘
src └──┘└────────┘└┘└────────────────────────────┘┴ └─────┘
typ └──┘└────────┘└┘└────────────────────────────┘┴└──┘└─────┘
doc └──┘ └┘ ┴ └─────┘
txt └──┘ └┘ ┴ └─────┘
par └──┘ └┘ ┴ └─────┘
pid └┘ └┘ ┴ ┴└────┘
st ───────────────┘└───────────────────────────────────┘┴└────┘└─
442 exact ⟨y, ys, hy⟩,
id ┴ └┘ └┘
src └────┘ └┘ └┘ ┴
typ └────┘ ┴└┘└┘└┘└┘┴
doc └────┘ └┘ └┘ ┴
txt └────┘ └┘ └┘ ┴
par └────┘ └┘ └┘ ┴
pid ┴ └┘ └┘ ┴
st ──────────────────┘└─
443 end
st ──┘
444
445 /-- The minimal distance from `x` to `s` is bounded by the distance from `y` to `s`, modulo
446 the distance between `x` and `y` -/
447 lemma inf_dist_le_inf_dist_add_dist : inf_dist x s ≤ inf_dist y s + dist x y :=
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴
src └──────┘ ┴ └──────┘ ┴ └──┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴
doc └──────┘ └──────┘
448 begin
st └─────
449 cases s.eq_empty_or_nonempty with hs hs,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘└─
450 { by simp [hs, dist_nonneg] },
id └┘ └─────────┘
src └────┘ └┘└─────────┘└┘
typ └────┘└┘└┘└─────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───┘ └┘└
451 { rw [inf_dist, inf_dist, dist_edist, ← ennreal.to_real_add (inf_edist_ne_top hs) (edist_ne_top _ _),
id └──────┘ └──────┘ └────────┘ └─────────────────┘ └──────────────┘ └┘ └──────────┘
src └──┘└──────┘└┘└──────┘└┘└────────┘└──┘└─────────────────┘┴ └──────────────┘┴ └┘ └──────────┘└──────
typ └──┘└──────┘└┘└──────┘└┘└────────┘└──┘└─────────────────┘┴ └──────────────┘┴└┘└┘ └──────────┘└──────
doc └──┘└──────┘└┘└──────┘└┘└────────┘└──┘ ┴ └──────────────┘┴ └┘ └──────────┘└──────
txt └──┘ └┘ └┘ └──┘ ┴ ┴ └┘ └──────
par └──┘ └┘ └┘ └──┘ ┴ ┴ └┘ └──────
pid └┘ └┘ └┘ └──┘ ┴ ┴ └┘ └──────
st ───────────────┘└────────┘└──────────┘└──────────────────────────────────────────────────────────────┘└─
452 ennreal.to_real_le_to_real (inf_edist_ne_top hs)],
id └────────────────────────┘ └──────────────┘ └┘
src ───────┘└────────────────────────┘┴ └──────────────┘┴ └┘
typ ───────┘└────────────────────────┘┴ └──────────────┘┴└┘└┘
doc ───────┘ ┴ └──────────────┘┴ └┘
txt ───────┘ ┴ ┴ └┘
par ───────┘ ┴ ┴ └┘
pid ───────┘ ┴ ┴ └┘
st ───────────────────────────────────────────────────────┘┴└─
453 { apply inf_edist_le_inf_edist_add_edist },
id └──────────────────────────────┘
src └────┘└──────────────────────────────┘┴
typ └────┘└──────────────────────────────┘┴
doc └────┘└──────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└─────────────────────────────────────┘└┘└
454 { simp [ennreal.add_eq_top, inf_edist_ne_top hs, edist_ne_top] }}
id └────────────────┘ └──────────────┘ └┘ └──────────┘
src └────┘└────────────────┘└┘└──────────────┘┴ └┘└──────────┘└┘
typ └────┘└────────────────┘└┘└──────────────┘┴└┘└┘└──────────┘└┘
doc └────┘ └┘└──────────────┘┴ └┘└──────────┘└┘
txt └────┘ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ └┘
pid ┴┴ └┘ ┴ └┘ ┴┴
st ──────────────────────────────────────────────────────────────────┘└──
455 end
st ──┘
456
457 variable (s)
458
459 /-- The minimal distance to a set is Lipschitz in point with constant 1 -/
460 lemma lipschitz_inf_dist_pt : lipschitz_with 1 (λx, inf_dist x s) :=
id └────────────┘ ┴ └──────┘ ┴ ┴
src └────────────┘ └──────┘
typ └────────────┘ ┴ └──────┘ ┴ ┴
doc └────────────┘ └──────┘
461 lipschitz_with.one_of_le_add $ λ x y, inf_dist_le_inf_dist_add_dist
id └──────────────────────────┘ ┴ ┴ └───────────────────────────┘
src └──────────────────────────┘ └───────────────────────────┘
typ └──────────────────────────┘ ┴ ┴ └───────────────────────────┘
doc └───────────────────────────┘
462
463 /-- The minimal distance to a set is uniformly continuous in point -/
464 lemma uniform_continuous_inf_dist_pt :
465 uniform_continuous (λx, inf_dist x s) :=
id └────────────────┘ ┴ └──────┘ ┴ ┴
src └────────────────┘ └──────┘
typ └────────────────┘ ┴ └──────┘ ┴ ┴
doc └──────┘
466 (lipschitz_inf_dist_pt s).to_uniform_continuous
id └───────────────────┘ ┴ └───────────────────┘
src └───────────────────┘ └───────────────────┘
typ └───────────────────┘ ┴ └───────────────────┘
doc └───────────────────┘ └───────────────────┘
467
468 /-- The minimal distance to a set is continuous in point -/
469 lemma continuous_inf_dist_pt : continuous (λx, inf_dist x s) :=
id └────────┘ ┴ └──────┘ ┴ ┴
src └────────┘ └──────┘
typ └────────┘ ┴ └──────┘ ┴ ┴
doc └────────┘ └──────┘
470 (uniform_continuous_inf_dist_pt s).continuous
id └────────────────────────────┘ ┴ └────────┘
src └────────────────────────────┘ └────────┘
typ └────────────────────────────┘ ┴ └────────┘
doc └────────────────────────────┘
471
472 variable {s}
473
474 /-- The minimal distance to a set and its closure coincide -/
475 lemma inf_dist_eq_closure : inf_dist x (closure s) = inf_dist x s :=
id └──────┘ ┴ └─────┘ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └─────┘ ┴ └──────┘
typ └──────┘ ┴ └─────┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └─────┘ └──────┘
476 by simp [inf_dist, inf_edist_closure]
id └──────┘ └───────────────┘
src └────┘└──────┘└┘└───────────────┘└─
typ └────┘└──────┘└┘└───────────────┘└─
doc └────┘└──────┘└┘└───────────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────────────────
477
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
478 /-- A point belongs to the closure of `s` iff its infimum distance to this set vanishes -/
479 lemma mem_closure_iff_inf_dist_zero (h : s.nonempty) : x ∈ closure s ↔ inf_dist x s = 0 :=
id ┴└───────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
src └───────┘ ┴ └─────┘ ┴ └──────┘ ┴
typ ┴└───────┘ ┴ ┴ └─────┘ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └───────┘ └─────┘ └──────┘
480 by simp [mem_closure_iff_inf_edist_zero, inf_dist, ennreal.to_real_eq_zero_iff, inf_edist_ne_top h]
id └────────────────────────────┘ └──────┘ └─────────────────────────┘ └──────────────┘ ┴
src └────┘└────────────────────────────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────────────┘┴ └─
typ └────┘└────────────────────────────┘└┘└──────┘└┘└─────────────────────────┘└┘└──────────────┘┴┴└─
doc └────┘└────────────────────────────┘└┘└──────┘└┘ └┘└──────────────┘┴ └─
txt └────┘ └┘ └┘ └┘ ┴ └─
par └────┘ └┘ └┘ └┘ ┴ └─
pid ┴┴ └┘ └┘ └┘ ┴ ┴└
st └─────────────────────────────────────────────────────────────────────────────────────────────────
481
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
482 /-- Given a closed set `s`, a point belongs to `s` iff its infimum distance to this set vanishes -/
483 lemma mem_iff_inf_dist_zero_of_closed (h : is_closed s) (hs : s.nonempty) :
id └───────┘ ┴ ┴└───────┘
src └───────┘ └───────┘
typ └───────┘ ┴ ┴└───────┘
doc └───────┘ └───────┘
484 x ∈ s ↔ inf_dist x s = 0 :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴
doc └──────┘
485 begin
st └─────
486 have := @mem_closure_iff_inf_dist_zero _ _ s x hs,
id └───────────────────────────┘ ┴ ┴ └┘
src └──────┘ └───────────────────────────┘└───┘ ┴ ┴
typ └──────┘ └───────────────────────────┘└───┘┴┴┴┴└┘
doc └──────┘ └───────────────────────────┘└───┘ ┴ ┴
txt └──────┘ └───┘ ┴ ┴
par └──────┘ └───┘ ┴ ┴
pid └───┘└─┘ └───┘ ┴ ┴
st ──────────────────────────────────────────────────┘└─
487 rwa closure_eq_iff_is_closed.2 h at this
id └──────────────────────┘ ┴
src └──┘└──────────────────────┘└─┘ └───────┘
typ └──┘└──────────────────────┘└─┘┴└───────┘
doc └──┘ └─┘ └───────┘
txt └──┘ └─┘ └───────┘
par └──┘ └─┘ └───────┘
pid ┴ └─┘ └──────┘┴
st ──────────────────────────────────────────┘
488 end
st └─┘
489
490 /-- The infimum distance is invariant under isometries -/
491 lemma inf_dist_image (hΦ : isometry Φ) :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
492 inf_dist (Φ x) (Φ '' t) = inf_dist x t :=
id └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──────┘ ┴ ┴
src └──────┘ └┘ ┴ └──────┘
typ └──────┘ ┴ ┴ ┴ └┘ ┴ ┴ └──────┘ ┴ ┴
doc └──────┘ └──────┘
493 by simp [inf_dist, inf_edist_image hΦ]
id └──────┘ └─────────────┘ └┘
src └────┘└──────┘└┘└─────────────┘┴ └─
typ └────┘└──────┘└┘└─────────────┘┴└┘└─
doc └────┘└──────┘└┘└─────────────┘┴ └─
txt └────┘ └┘ ┴ └─
par └────┘ └┘ ┴ └─
pid ┴┴ └┘ ┴ ┴└
st └────────────────────────────────────
494
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
495 /-- The Hausdorff distance between two sets is the smallest nonnegative `r` such that each set is
496 included in the `r`-neighborhood of the other. If there is no such `r`, it is defined to
497 be `0`, arbitrarily -/
498 def Hausdorff_dist (s t : set α) : ℝ := ennreal.to_real (Hausdorff_edist s t)
id └─┘ ┴ ┴ └─────────────┘ └─────────────┘ ┴ ┴
src └─┘ ┴ └─────────────┘ └─────────────┘
typ └─┘ ┴ ┴ └─────────────┘ └─────────────┘ ┴ ┴
doc └─────────────┘ └─────────────┘
499
500 /-- The Hausdorff distance is nonnegative -/
501 lemma Hausdorff_dist_nonneg : 0 ≤ Hausdorff_dist s t :=
id ┴ └────────────┘ ┴ ┴
src ┴ └────────────┘
typ ┴ └────────────┘ ┴ ┴
doc └────────────┘
502 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
503
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
504 /-- If two sets are nonempty and bounded in a metric space, they are at finite Hausdorff edistance -/
505 lemma Hausdorff_edist_ne_top_of_nonempty_of_bounded (hs : s.nonempty) (ht : t.nonempty)
id ┴└───────┘ ┴└───────┘
src └───────┘ └───────┘
typ ┴└───────┘ ┴└───────┘
doc └───────┘ └───────┘
506 (bs : bounded s) (bt : bounded t) : Hausdorff_edist s t ≠ ⊤ :=
id └─────┘ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src └─────┘ └─────┘ └─────────────┘ ┴ ┴
typ └─────┘ ┴ └─────┘ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────┘ └─────┘ └─────────────┘
507 begin
st └─────
508 rcases hs with ⟨cs, hcs⟩,
id └┘
src └─────┘ └─────────────┘
typ └─────┘└┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ─────────────────────────┘└─
509 rcases ht with ⟨ct, hct⟩,
id └┘
src └─────┘ └─────────────┘
typ └─────┘└┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st ─────────────────────────┘└─
510 rcases (bounded_iff_subset_ball ct).1 bs with ⟨rs, hrs⟩,
id └─────────────────────┘ └┘ └┘
src └─────┘ └─────────────────────┘┴ └──┘ └─────────────┘
typ └─────┘ └─────────────────────┘┴└┘└──┘└┘└─────────────┘
doc └─────┘ └─────────────────────┘┴ └──┘ └─────────────┘
txt └─────┘ ┴ └──┘ └─────────────┘
par └─────┘ ┴ └──┘ └─────────────┘
pid ┴ ┴ └──┘ └─────────────┘
st ────────────────────────────────────────────────────────┘└─
511 rcases (bounded_iff_subset_ball cs).1 bt with ⟨rt, hrt⟩,
id └─────────────────────┘ └┘ └┘
src └─────┘ └─────────────────────┘┴ └──┘ └─────────────┘
typ └─────┘ └─────────────────────┘┴└┘└──┘└┘└─────────────┘
doc └─────┘ └─────────────────────┘┴ └──┘ └─────────────┘
txt └─────┘ ┴ └──┘ └─────────────┘
par └─────┘ ┴ └──┘ └─────────────┘
pid ┴ ┴ └──┘ └─────────────┘
st ────────────────────────────────────────────────────────┘└─
512 have : Hausdorff_edist s t ≤ ennreal.of_real (max rs rt),
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ └─┘ └┘ └┘
src └─────┘└─────────────┘┴ ┴ ┴┴┴└─────────────┘┴ └─┘┴ ┴ ┴
typ └─────┘└─────────────┘┴┴┴┴┴┴┴└─────────────┘┴ └─┘┴└┘┴└┘┴
doc └─────┘└─────────────┘┴ ┴ ┴ ┴└─────────────┘┴ ┴ ┴ ┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────┘└─
513 { apply Hausdorff_edist_le_of_mem_edist,
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘
typ └────┘└─────────────────────────────┘
doc └────┘└─────────────────────────────┘
txt └────┘
par └────┘
pid ┴
st ───┘└───────────────────────────────────┘└─
514 { assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
515 existsi [ct, hct],
id └┘ └─┘
src └───────┘ └┘ ┴
typ └───────┘└┘└┘└─┘┴
doc └───────┘ └┘ ┴
txt └───────┘ └┘ ┴
par └───────┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────┘└─
516 have : dist x ct ≤ max rs rt := le_trans (hrs xs) (le_max_left _ _),
id └──┘ ┴ └┘ └─┘ └┘ └┘ └──────┘ └─┘ └┘ └─────────┘
src └─────┘└──┘┴ ┴ ┴ ┴└─┘┴ ┴ └──┘└──────┘┴ ┴ └┘ └─────────┘└───┘
typ └─────┘└──┘┴┴┴└┘┴ ┴└─┘┴└┘┴└┘└──┘└──────┘┴ └─┘┴└┘└┘ └─────────┘└───┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
st ────────────────────────────────────────────────────────────────────────┘└─
517 rwa [edist_dist, ennreal.of_real_le_of_real_iff],
id └────────┘ └────────────────────────────┘
src └───┘└────────┘└┘└────────────────────────────┘┴
typ └───┘└────────┘└┘└────────────────────────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────┘└──────────────────────────────┘┴└─
518 exact le_trans dist_nonneg this },
id └──────┘ └─────────┘ └──┘
src └────┘└──────┘┴└─────────┘┴ ┴
typ └────┘└──────┘┴└─────────┘┴└──┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└┘└
519 { assume x xt,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────────┘└─
520 existsi [cs, hcs],
id └┘ └─┘
src └───────┘ └┘ ┴
typ └───────┘└┘└┘└─┘┴
doc └───────┘ └┘ ┴
txt └───────┘ └┘ ┴
par └───────┘ └┘ ┴
pid └┘ └┘ ┴
st ──────────────────────┘└─
521 have : dist x cs ≤ max rs rt := le_trans (hrt xt) (le_max_right _ _),
id └──┘ ┴ └┘ └─┘ └┘ └┘ └──────┘ └─┘ └┘ └──────────┘
src └─────┘└──┘┴ ┴ ┴ ┴└─┘┴ ┴ └──┘└──────┘┴ ┴ └┘ └──────────┘└───┘
typ └─────┘└──┘┴┴┴└┘┴ ┴└─┘┴└┘┴└┘└──┘└──────┘┴ └─┘┴└┘└┘ └──────────┘└───┘
doc └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
txt └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
par └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴ ┴ └┘ └───┘
st ─────────────────────────────────────────────────────────────────────────┘└─
522 rwa [edist_dist, ennreal.of_real_le_of_real_iff],
id └────────┘ └────────────────────────────┘
src └───┘└────────┘└┘└────────────────────────────┘┴
typ └───┘└────────┘└┘└────────────────────────────┘┴
doc └───┘ └┘ ┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st ────────────────────┘└──────────────────────────────┘┴└─
523 exact le_trans dist_nonneg this }},
id └──────┘ └─────────┘ └──┘
src └────┘└──────┘┴└─────────┘┴ ┴
typ └────┘└──────┘┴└─────────┘┴└──┘┴
doc └────┘ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘└─┘└
524 exact ennreal.lt_top_iff_ne_top.1 (lt_of_le_of_lt this (by simp [lt_top_iff_ne_top]))
id └───────────────────────┘ └────────────┘ └──┘ └───────────────┘
src └────┘└───────────────────────┘└─┘ └────────────┘┴ ┴ ┴└────┘└───────────────┘┴└─┘
typ └────┘└───────────────────────┘└─┘ └────────────┘┴└──┘┴ ┴└────┘└───────────────┘┴└─┘
doc └────┘ └─┘ ┴ ┴ ┴└────┘ ┴└─┘
txt └────┘ └─┘ ┴ ┴ ┴└────┘ ┴└─┘
par └────┘ └─┘ ┴ ┴ ┴└────┘ ┴└─┘
pid ┴ └─┘ ┴ ┴ └─────┘ └─┘┴
st ───────────────────────────────────────────────────────────┘└───────────────────────┘└─┘
525 end
st └─┘
526
527 /-- The Hausdorff distance between a set and itself is zero -/
528 @[simp] lemma Hausdorff_dist_self_zero : Hausdorff_dist s s = 0 :=
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴
doc └──┘ └────────────┘
529 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
530
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
531 /-- The Hausdorff distance from `s` to `t` and from `t` to `s` coincide -/
532 lemma Hausdorff_dist_comm : Hausdorff_dist s t = Hausdorff_dist t s :=
id └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ ┴ └────────────┘
typ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘ └────────────┘
533 by simp [Hausdorff_dist, Hausdorff_edist_comm]
id └────────────┘ └──────────────────┘
src └────┘└────────────┘└┘└──────────────────┘└─
typ └────┘└────────────┘└┘└──────────────────┘└─
doc └────┘└────────────┘└┘└──────────────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────────────────
534
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
535 /-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
536 value ∞ instead, use `Hausdorff_edist`, which takes values in ennreal) -/
537 @[simp] lemma Hausdorff_dist_empty : Hausdorff_dist s ∅ = 0 :=
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ ┴
typ └────────────┘ ┴ ┴ ┴
doc └──┘ └────────────┘
538 begin
st └─────
539 cases s.eq_empty_or_nonempty with h h,
id └────────────────────┘
src └────┘└────────────────────┘└───────┘
typ └────┘└────────────────────┘└───────┘
doc └────┘ └───────┘
txt └────┘ └───────┘
par └────┘ └───────┘
pid ┴ └───────┘
st ──────────────────────────────────────┘└─
540 { simp [h] },
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st ───┘└───────┘└┘└
541 { simp [Hausdorff_dist, Hausdorff_edist_empty h] }
id └────────────┘ └───────────────────┘ ┴
src └────┘└────────────┘└┘└───────────────────┘┴ └┘
typ └────┘└────────────┘└┘└───────────────────┘┴┴└┘
doc └────┘└────────────┘└┘└───────────────────┘┴ └┘
txt └────┘ └┘ ┴ └┘
par └────┘ └┘ ┴ └┘
pid ┴┴ └┘ ┴ ┴┴
st ──────────────────────────────────────────────────┘└─
542 end
st ──┘
543
544 /-- The Hausdorff distance to the empty set vanishes (if you want to have the more reasonable
545 value ∞ instead, use `Hausdorff_edist`, which takes values in ennreal) -/
546 @[simp] lemma Hausdorff_dist_empty' : Hausdorff_dist ∅ s = 0 :=
id └────────────┘ ┴ ┴ ┴
src └────────────┘ ┴ ┴
typ └────────────┘ ┴ ┴ ┴
doc └──┘ └────────────┘
547 by simp [Hausdorff_dist_comm]
id └─────────────────┘
src └────┘└─────────────────┘└─
typ └────┘└─────────────────┘└─
doc └────┘└─────────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────────────────────
548
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
549 /-- Bounding the Hausdorff distance by bounding the distance of any point
550 in each set to the other set -/
551 lemma Hausdorff_dist_le_of_inf_dist {r : ℝ} (hr : r ≥ 0)
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
552 (H1 : ∀x ∈ s, inf_dist x t ≤ r) (H2 : ∀x ∈ t, inf_dist x s ≤ r) :
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └──────┘ └──────┘
553 Hausdorff_dist s t ≤ r :=
id └────────────┘ ┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘
554 begin
st └─────
555 by_cases h1 : Hausdorff_edist s t = ⊤,
id └─────────────┘ ┴ ┴ ┴ ┴
src └───────┘ └─┘└─────────────┘┴ ┴ ┴┴┴┴
typ └───────┘ └─┘└─────────────┘┴┴┴┴┴┴┴┴
doc └───────┘ └─┘└─────────────┘┴ ┴ ┴ ┴
txt └───────┘ └─┘ ┴ ┴ ┴ ┴
par └───────┘ └─┘ ┴ ┴ ┴ ┴
pid ┴ └─┘ ┴ ┴ ┴ ┴
st ──────────────────────────────────────┘
556 by rwa [Hausdorff_dist, h1, ennreal.top_to_real],
id └────────────┘ └┘ └─────────────────┘
src └───┘└────────────┘└┘ └┘└─────────────────┘┴
typ └───┘└────────────┘└┘└┘└┘└─────────────────┘┴
doc └───┘└────────────┘└┘ └┘ ┴
txt └───┘ └┘ └┘ ┴
par └───┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st └────────────┘└──┘└───────────────────┘┴└─
557 cases s.eq_empty_or_nonempty with hs hs,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘
558 by rwa [hs, Hausdorff_dist_empty'],
id └┘ └───────────────────┘
src └───┘ └┘└───────────────────┘┴
typ └───┘└┘└┘└───────────────────┘┴
doc └───┘ └┘└───────────────────┘┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st └┘└─────────────────────┘┴└─
559 cases t.eq_empty_or_nonempty with ht ht,
id └────────────────────┘
src └────┘└────────────────────┘└─────────┘
typ └────┘└────────────────────┘└─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ └─────────┘
st ────────────────────────────────────────┘
560 by rwa [ht, Hausdorff_dist_empty],
id └┘ └──────────────────┘
src └───┘ └┘└──────────────────┘┴
typ └───┘└┘└┘└──────────────────┘┴
doc └───┘ └┘└──────────────────┘┴
txt └───┘ └┘ ┴
par └───┘ └┘ ┴
pid └┘ └┘ ┴
st └┘└────────────────────┘┴└─
561 have : Hausdorff_edist s t ≤ ennreal.of_real r,
id └─────────────┘ ┴ ┴ ┴ └─────────────┘ ┴
src └─────┘└─────────────┘┴ ┴ ┴┴┴└─────────────┘┴
typ └─────┘└─────────────┘┴┴┴┴┴┴┴└─────────────┘┴┴
doc └─────┘└─────────────┘┴ ┴ ┴ ┴└─────────────┘┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└─
562 { apply Hausdorff_edist_le_of_inf_edist _ _,
id └─────────────────────────────┘
src └────┘└─────────────────────────────┘└──┘
typ └────┘└─────────────────────────────┘└──┘
doc └────┘└─────────────────────────────┘└──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴ └──┘
st ───┘└───────────────────────────────────────┘└─
563 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ─────┘└─────────┘└─
564 have I := H1 x hx,
id └┘ ┴ └┘
src └────────┘ ┴ ┴
typ └────────┘└┘┴┴┴└┘
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ──────────────────────┘└─
565 rwa [inf_dist, ← ennreal.to_real_of_real hr,
id └──────┘ └─────────────────────┘ └┘
src └───┘└──────┘└──┘└─────────────────────┘┴ └─
typ └───┘└──────┘└──┘└─────────────────────┘┴└┘└─
doc └───┘└──────┘└──┘ ┴ └─
txt └───┘ └──┘ ┴ └─
par └───┘ └──┘ ┴ └─
pid └┘ └──┘ ┴ └─
st ──────────────────┘└────────────────────────────┘└─
566 ennreal.to_real_le_to_real (inf_edist_ne_top ht) ennreal.of_real_ne_top] at I },
id └────────────────────────┘ └──────────────┘ └┘ └────────────────────┘
src ──────────┘└────────────────────────┘┴ └──────────────┘┴ └┘└────────────────────┘└─────┘
typ ──────────┘└────────────────────────┘┴ └──────────────┘┴└┘└┘└────────────────────┘└─────┘
doc ──────────┘ ┴ └──────────────┘┴ └┘ └─────┘
txt ──────────┘ ┴ ┴ └┘ └─────┘
par ──────────┘ ┴ ┴ └┘ └─────┘
pid ──────────┘ ┴ ┴ └┘ ┴└───┘┴
st ─────────────────────────────────────────────────────────────────────────────────┘┴└────┘└┘└
567 { assume x hx,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ────────────────┘└─
568 have I := H2 x hx,
id └┘ ┴ └┘
src └────────┘ ┴ ┴
typ └────────┘└┘┴┴┴└┘
doc └────────┘ ┴ ┴
txt └────────┘ ┴ ┴
par └────────┘ ┴ ┴
pid └────┘┴└─┘ ┴ ┴
st ──────────────────────┘└─
569 rwa [inf_dist, ← ennreal.to_real_of_real hr,
id └──────┘ └─────────────────────┘ └┘
src └───┘└──────┘└──┘└─────────────────────┘┴ └─
typ └───┘└──────┘└──┘└─────────────────────┘┴└┘└─
doc └───┘└──────┘└──┘ ┴ └─
txt └───┘ └──┘ ┴ └─
par └───┘ └──┘ ┴ └─
pid └┘ └──┘ ┴ └─
st ──────────────────┘└────────────────────────────┘└─
570 ennreal.to_real_le_to_real (inf_edist_ne_top hs) ennreal.of_real_ne_top] at I }},
id └────────────────────────┘ └──────────────┘ └┘ └────────────────────┘
src ──────────┘└────────────────────────┘┴ └──────────────┘┴ └┘└────────────────────┘└─────┘
typ ──────────┘└────────────────────────┘┴ └──────────────┘┴└┘└┘└────────────────────┘└─────┘
doc ──────────┘ ┴ └──────────────┘┴ └┘ └─────┘
txt ──────────┘ ┴ ┴ └┘ └─────┘
par ──────────┘ ┴ ┴ └┘ └─────┘
pid ──────────┘ ┴ ┴ └┘ ┴└───┘┴
st ─────────────────────────────────────────────────────────────────────────────────┘┴└────┘└─┘└
571 rwa [Hausdorff_dist, ← ennreal.to_real_of_real hr,
id └────────────┘ └─────────────────────┘ └┘
src └───┘└────────────┘└──┘└─────────────────────┘┴ └─
typ └───┘└────────────┘└──┘└─────────────────────┘┴└┘└─
doc └───┘└────────────┘└──┘ ┴ └─
txt └───┘ └──┘ ┴ └─
par └───┘ └──┘ ┴ └─
pid └┘ └──┘ ┴ └─
st ────────────────────┘└────────────────────────────┘└─
572 ennreal.to_real_le_to_real h1 ennreal.of_real_ne_top]
id └────────────────────────┘ └┘ └────────────────────┘
src ──────┘└────────────────────────┘┴ ┴└────────────────────┘└┘
typ ──────┘└────────────────────────┘┴└┘┴└────────────────────┘└┘
doc ──────┘ ┴ ┴ └┘
txt ──────┘ ┴ ┴ └┘
par ──────┘ ┴ ┴ └┘
pid ──────┘ ┴ ┴ ┴┴
st ──────────────────────────────────────────────────────────┘┴┴
573 end
st └─┘
574
575 /-- Bounding the Hausdorff distance by exhibiting, for any point in each set,
576 another point in the other set at controlled distance -/
577 lemma Hausdorff_dist_le_of_mem_dist {r : ℝ} (hr : 0 ≤ r)
id ┴ ┴ ┴
src ┴ ┴
typ ┴ ┴ ┴
578 (H1 : ∀x ∈ s, ∃y ∈ t, dist x y ≤ r) (H2 : ∀x ∈ t, ∃y ∈ s, dist x y ≤ r) :
id ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
src ┴ ┴ └──┘ ┴ ┴ ┴ └──┘ ┴
typ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
579 Hausdorff_dist s t ≤ r :=
id └────────────┘ ┴ ┴ ┴ ┴
src └────────────┘ ┴
typ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘
580 begin
st └─────
581 apply Hausdorff_dist_le_of_inf_dist hr,
id └───────────────────────────┘ └┘
src └────┘└───────────────────────────┘┴
typ └────┘└───────────────────────────┘┴└┘
doc └────┘└───────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───────────────────────────────────────┘└─
582 { assume x xs,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ───┘└─────────┘└─
583 rcases H1 x xs with ⟨y, yt, hy⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ──────────────────────────────────┘└─
584 exact le_trans (inf_dist_le_dist_of_mem yt) hy },
id └──────┘ └─────────────────────┘ └┘ └┘
src └────┘└──────┘┴ └─────────────────────┘┴ └┘ ┴
typ └────┘└──────┘┴ └─────────────────────┘┴└┘└┘└┘┴
doc └────┘ ┴ └─────────────────────┘┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────┘└┘└
585 { assume x xt,
src └─────────┘
typ └─────────┘
doc └─────────┘
txt └─────────┘
par └─────────┘
pid └─────────┘
st ──────────────┘└─
586 rcases H2 x xt with ⟨y, ys, hy⟩,
id └┘ ┴ └┘
src └─────┘ ┴ ┴ └───────────────┘
typ └─────┘└┘┴┴┴└┘└───────────────┘
doc └─────┘ ┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ──────────────────────────────────┘└─
587 exact le_trans (inf_dist_le_dist_of_mem ys) hy }
id └──────┘ └─────────────────────┘ └┘ └┘
src └────┘└──────┘┴ └─────────────────────┘┴ └┘ ┴
typ └────┘└──────┘┴ └─────────────────────┘┴└┘└┘└┘┴
doc └────┘ ┴ └─────────────────────┘┴ └┘ ┴
txt └────┘ ┴ ┴ └┘ ┴
par └────┘ ┴ ┴ └┘ ┴
pid ┴ ┴ ┴ └┘ ┴
st ──────────────────────────────────────────────────┘└─
588 end
st ──┘
589
590 /-- The Hausdorff distance is controlled by the diameter of the union -/
591 lemma Hausdorff_dist_le_diam (hs : s.nonempty) (bs : bounded s) (ht : t.nonempty) (bt : bounded t) :
id ┴└───────┘ └─────┘ ┴ ┴└───────┘ └─────┘ ┴
src └───────┘ └─────┘ └───────┘ └─────┘
typ ┴└───────┘ └─────┘ ┴ ┴└───────┘ └─────┘ ┴
doc └───────┘ └─────┘ └───────┘ └─────┘
592 Hausdorff_dist s t ≤ diam (s ∪ t) :=
id └────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
src └────────────┘ ┴ └──┘ ┴
typ └────────────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴
doc └────────────┘ └──┘
593 begin
st └─────
594 rcases hs with ⟨x, xs⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
595 rcases ht with ⟨y, yt⟩,
id └┘
src └─────┘ └───────────┘
typ └─────┘└┘└───────────┘
doc └─────┘ └───────────┘
txt └─────┘ └───────────┘
par └─────┘ └───────────┘
pid ┴ └───────────┘
st ───────────────────────┘└─
596 refine Hausdorff_dist_le_of_mem_dist diam_nonneg _ _,
id └───────────────────────────┘ └─────────┘
src └─────┘└───────────────────────────┘┴└─────────┘└──┘
typ └─────┘└───────────────────────────┘┴└─────────┘└──┘
doc └─────┘└───────────────────────────┘┴└─────────┘└──┘
txt └─────┘ ┴ └──┘
par └─────┘ ┴ └──┘
pid ┴ ┴ └──┘
st ─────────────────────────────────────────────────────┘└─
597 { exact λz hz, ⟨y, yt, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩)
id ┴ └─────────────────┘ └───────────┘ └┘ └┘
src └─────┘ └────┘ └┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘ └──
typ └─────┘ └────┘ ┴└┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘└┘└┘└──
doc └─────┘ └────┘ └┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘ └──
txt └─────┘ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
par └─────┘ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
pid └┘ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
st ───┘└────────────────────────────────────────────────────────────────────
598 (subset_union_left _ _ hz) (subset_union_right _ _ yt)⟩ },
id └───────────────┘ └────────────────┘ └┘
src ─────┘ └───────────────┘└───┘ └┘ └────────────────┘└───┘ └─┘
typ ─────┘ └───────────────┘└───┘ └┘ └────────────────┘└───┘└┘└─┘
doc ─────┘ └───┘ └┘ └───┘ └─┘
txt ─────┘ └───┘ └┘ └───┘ └─┘
par ─────┘ └───┘ └┘ └───┘ └─┘
pid ─────┘ └───┘ └┘ └───┘ └┘┴
st ─────────────────────────────────────────────────────────────┘└┘└
599 { exact λz hz, ⟨x, xs, dist_le_diam_of_mem (bounded_union.2 ⟨bs, bt⟩)
id ┴ └─────────────────┘ └───────────┘ └┘ └┘
src └────┘ └────┘ └┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘ └──
typ └────┘ └────┘ ┴└┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘└┘└┘└──
doc └────┘ └────┘ └┘ └┘└─────────────────┘┴ └───────────┘└─┘ └┘ └──
txt └────┘ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
par └────┘ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
pid ┴ └────┘ └┘ └┘ ┴ └─┘ └┘ └──
st ────────────────────────────────────────────────────────────────────────
600 (subset_union_right _ _ hz) (subset_union_left _ _ xs)⟩ }
id └────────────────┘ └───────────────┘ └┘
src ─────┘ └────────────────┘└───┘ └┘ └───────────────┘└───┘ └─┘
typ ─────┘ └────────────────┘└───┘ └┘ └───────────────┘└───┘└┘└─┘
doc ─────┘ └───┘ └┘ └───┘ └─┘
txt ─────┘ └───┘ └┘ └───┘ └─┘
par ─────┘ └───┘ └┘ └───┘ └─┘
pid ─────┘ └───┘ └┘ └───┘ └┘┴
st ─────────────────────────────────────────────────────────────┘└─
601 end
st ──┘
602
603 /-- The distance to a set is controlled by the Hausdorff distance -/
604 lemma inf_dist_le_Hausdorff_dist_of_mem (hx : x ∈ s) (fin : Hausdorff_edist s t ≠ ⊤) :
id ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
src ┴ └─────────────┘ ┴ ┴
typ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
605 inf_dist x t ≤ Hausdorff_dist s t :=
id └──────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └──────┘ ┴ └────────────┘
typ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └──────┘ └────────────┘
606 begin
st └─────
607 have ht : t.nonempty := nonempty_of_Hausdorff_edist_ne_top ⟨x, hx⟩ fin,
id └────────┘ └────────────────────────────────┘ ┴ └┘ └─┘
src └────────┘└────────┘└──┘└────────────────────────────────┘┴ └┘ └┘└─┘
typ └────────┘└────────┘└──┘└────────────────────────────────┘┴ ┴└┘└┘└┘└─┘
doc └────────┘└────────┘└──┘└────────────────────────────────┘┴ └┘ └┘
txt └────────┘ └──┘ ┴ └┘ └┘
par └────────┘ └──┘ ┴ └┘ └┘
pid └─────┘└─┘ └──┘ ┴ └┘ └┘
st ───────────────────────────────────────────────────────────────────────┘└─
608 rw [Hausdorff_dist, inf_dist, ennreal.to_real_le_to_real (inf_edist_ne_top ht) fin],
id └────────────┘ └──────┘ └────────────────────────┘ └──────────────┘ └┘ └─┘
src └──┘└────────────┘└┘└──────┘└┘└────────────────────────┘┴ └──────────────┘┴ └┘└─┘┴
typ └──┘└────────────┘└┘└──────┘└┘└────────────────────────┘┴ └──────────────┘┴└┘└┘└─┘┴
doc └──┘└────────────┘└┘└──────┘└┘ ┴ └──────────────┘┴ └┘ ┴
txt └──┘ └┘ └┘ ┴ ┴ └┘ ┴
par └──┘ └┘ └┘ ┴ ┴ └┘ ┴
pid └┘ └┘ └┘ ┴ ┴ └┘ ┴
st ───────────────────┘└────────┘└────────────────────────────────────────────────────┘└──
609 exact inf_edist_le_Hausdorff_edist_of_mem hx
id └─────────────────────────────────┘ └┘
src └────┘└─────────────────────────────────┘┴ ┴
typ └────┘└─────────────────────────────────┘┴└┘┴
doc └────┘└─────────────────────────────────┘┴ ┴
txt └────┘ ┴ ┴
par └────┘ ┴ ┴
pid ┴ ┴ ┴
st ──────────────────────────────────────────────┘
610 end
st └─┘
611
612 /-- If the Hausdorff distance is `<r`, then any point in one of the sets is at distance
613 `<r` of a point in the other set -/
614 lemma exists_dist_lt_of_Hausdorff_dist_lt {r : ℝ} (h : x ∈ s) (H : Hausdorff_dist s t < r)
id ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘
615 (fin : Hausdorff_edist s t ≠ ⊤) : ∃y∈t, dist x y < r :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴ ┴ └──┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
doc └─────────────┘
616 begin
st └─────
617 have r0 : 0 < r := lt_of_le_of_lt (Hausdorff_dist_nonneg) H,
id ┴ ┴ └────────────┘ └───────────────────┘ ┴
src └──────────┘┴┴ └──┘└────────────┘┴ └───────────────────┘└┘
typ └──────────┘┴┴┴└──┘└────────────┘┴ └───────────────────┘└┘┴
doc └──────────┘ ┴ └──┘ ┴ └───────────────────┘└┘
txt └──────────┘ ┴ └──┘ ┴ └┘
par └──────────┘ ┴ └──┘ ┴ └┘
pid └─────┘└───┘ ┴ └──┘ ┴ └┘
st ────────────────────────────────────────────────────────────┘└─
618 have : Hausdorff_edist s t < ennreal.of_real r,
id └─────────────┘ ┴ ┴ └─────────────┘ ┴
src └─────┘└─────────────┘┴ ┴ ┴ ┴└─────────────┘┴
typ └─────┘└─────────────┘┴┴┴┴┴ ┴└─────────────┘┴┴
doc └─────┘└─────────────┘┴ ┴ ┴ ┴└─────────────┘┴
txt └─────┘ ┴ ┴ ┴ ┴ ┴
par └─────┘ ┴ ┴ ┴ ┴ ┴
pid └───┘└┘ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘
619 by rwa [Hausdorff_dist, ← ennreal.to_real_of_real (le_of_lt r0),
id └────────────┘ └─────────────────────┘ └──────┘ └┘
src └───┘└────────────┘└──┘└─────────────────────┘┴ └──────┘┴ └──
typ └───┘└────────────┘└──┘└─────────────────────┘┴ └──────┘┴└┘└──
doc └───┘└────────────┘└──┘ ┴ ┴ └──
txt └───┘ └──┘ ┴ ┴ └──
par └───┘ └──┘ ┴ ┴ └──
pid └┘ └──┘ ┴ ┴ └──
st └────────────┘└───────────────────────────────────────┘└─
620 ennreal.to_real_lt_to_real fin (ennreal.of_real_ne_top)] at H,
id └────────────────────────┘ └─┘ └────────────────────┘
src ───────────┘└────────────────────────┘┴└─┘┴ └────────────────────┘└─────┘
typ ───────────┘└────────────────────────┘┴└─┘┴ └────────────────────┘└─────┘
doc ───────────┘ ┴ ┴ └─────┘
txt ───────────┘ ┴ ┴ └─────┘
par ───────────┘ ┴ ┴ └─────┘
pid ───────────┘ ┴ ┴ └┘└───┘
st ──────────────────────────────────────────────────────────────────┘┴ └─
621 rcases exists_edist_lt_of_Hausdorff_edist_lt h this with ⟨y, hy, yr⟩,
id └───────────────────────────────────┘ ┴ └──┘
src └─────┘└───────────────────────────────────┘┴ ┴ └───────────────┘
typ └─────┘└───────────────────────────────────┘┴┴┴└──┘└───────────────┘
doc └─────┘└───────────────────────────────────┘┴ ┴ └───────────────┘
txt └─────┘ ┴ ┴ └───────────────┘
par └─────┘ ┴ ┴ └───────────────┘
pid ┴ ┴ ┴ └───────────────┘
st ─────────────────────────────────────────────────────────────────────┘└─
622 rw [edist_dist, ennreal.of_real_lt_of_real_iff r0] at yr,
id └────────┘ └────────────────────────────┘ └┘
src └──┘└────────┘└┘└────────────────────────────┘┴ └─────┘
typ └──┘└────────┘└┘└────────────────────────────┘┴└┘└─────┘
doc └──┘ └┘ ┴ └─────┘
txt └──┘ └┘ ┴ └─────┘
par └──┘ └┘ ┴ └─────┘
pid └┘ └┘ ┴ ┴└────┘
st ───────────────┘└─────────────────────────────────┘┴└────┘└─
623 exact ⟨y, hy, yr⟩
id ┴ └┘ └┘
src └────┘ └┘ └┘ └┘
typ └────┘ ┴└┘└┘└┘└┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid ┴ └┘ └┘ ┴┴
st ───────────────────┘
624 end
st └─┘
625
626 /-- If the Hausdorff distance is `<r`, then any point in one of the sets is at distance
627 `<r` of a point in the other set -/
628 lemma exists_dist_lt_of_Hausdorff_dist_lt' {r : ℝ} (h : y ∈ t) (H : Hausdorff_dist s t < r)
id ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └────────────┘ ┴
typ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴
doc └────────────┘
629 (fin : Hausdorff_edist s t ≠ ⊤) : ∃x∈s, dist x y < r :=
id └─────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ ┴ ┴ └──┘ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ ┴┴ ┴┴ └──┘ ┴ ┴ ┴ ┴
doc └─────────────┘
630 begin
st └─────
631 rw Hausdorff_dist_comm at H,
id └─────────────────┘
src └─┘└─────────────────┘└───┘
typ └─┘└─────────────────┘└───┘
doc └─┘└─────────────────┘└───┘
txt └─┘ └───┘
par └─┘ └───┘
pid ┴ └───┘
st ────────────────────────────┘└─
632 rw Hausdorff_edist_comm at fin,
id └──────────────────┘
src └─┘└──────────────────┘└─────┘
typ └─┘└──────────────────┘└─────┘
doc └─┘└──────────────────┘└─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────────┘└─
633 simpa [dist_comm] using exists_dist_lt_of_Hausdorff_dist_lt h H fin
id └───────┘ └─────────────────────────────────┘ ┴ ┴ └─┘
src └─────┘└───────┘└──────┘└─────────────────────────────────┘┴ ┴ ┴└─┘┴
typ └─────┘└───────┘└──────┘└─────────────────────────────────┘┴┴┴┴┴└─┘┴
doc └─────┘ └──────┘└─────────────────────────────────┘┴ ┴ ┴ ┴
txt └─────┘ └──────┘ ┴ ┴ ┴ ┴
par └─────┘ └──────┘ ┴ ┴ ┴ ┴
pid ┴┴ ┴┴└────┘ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────┘
634 end
st └─┘
635
636 /-- The infimum distance to `s` and `t` are the same, up to the Hausdorff distance
637 between `s` and `t` -/
638 lemma inf_dist_le_inf_dist_add_Hausdorff_dist (fin : Hausdorff_edist s t ≠ ⊤) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
639 inf_dist x t ≤ inf_dist x s + Hausdorff_dist s t :=
id └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └──────┘ ┴ └──────┘ ┴ └────────────┘
typ └──────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └──────┘ └──────┘ └────────────┘
640 begin
st └─────
641 rcases empty_or_nonempty_of_Hausdorff_edist_ne_top fin with ⟨hs,ht⟩|⟨hs,ht⟩,
id └─────────────────────────────────────────┘ └─┘
src └─────┘└─────────────────────────────────────────┘┴└─┘└───────────────────┘
typ └─────┘└─────────────────────────────────────────┘┴└─┘└───────────────────┘
doc └─────┘ ┴ └───────────────────┘
txt └─────┘ ┴ └───────────────────┘
par └─────┘ ┴ └───────────────────┘
pid ┴ ┴ └───────────────────┘
st ────────────────────────────────────────────────────────────────────────────┘└─
642 { simp only [hs, ht, Hausdorff_dist_empty, inf_dist_empty, zero_add] },
id └┘ └┘ └──────────────────┘ └────────────┘ └──────┘
src └─────────┘ └┘ └┘└──────────────────┘└┘└────────────┘└┘└──────┘└┘
typ └─────────┘└┘└┘└┘└┘└──────────────────┘└┘└────────────┘└┘└──────┘└┘
doc └─────────┘ └┘ └┘└──────────────────┘└┘└────────────┘└┘ └┘
txt └─────────┘ └┘ └┘ └┘ └┘ └┘
par └─────────┘ └┘ └┘ └┘ └┘ └┘
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ ┴┴
st ───┘└─────────────────────────────────────────────────────────────────┘└┘└
643 rw [inf_dist, inf_dist, Hausdorff_dist, ← ennreal.to_real_add (inf_edist_ne_top hs) fin,
id └──────┘ └──────┘ └────────────┘ └─────────────────┘ └──────────────┘ └┘ └─┘
src └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘└─────────────────┘┴ └──────────────┘┴ └┘└─┘└─
typ └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘└─────────────────┘┴ └──────────────┘┴└┘└┘└─┘└─
doc └──┘└──────┘└┘└──────┘└┘└────────────┘└──┘ ┴ └──────────────┘┴ └┘ └─
txt └──┘ └┘ └┘ └──┘ ┴ ┴ └┘ └─
par └──┘ └┘ └┘ └──┘ ┴ ┴ └┘ └─
pid └┘ └┘ └┘ └──┘ ┴ ┴ └┘ └─
st ─────────────┘└────────┘└──────────────┘└───────────────────────────────────────────────┘└─
644 ennreal.to_real_le_to_real (inf_edist_ne_top ht)],
id └────────────────────────┘ └──────────────┘ └┘
src ─────┘└────────────────────────┘┴ └──────────────┘┴ └┘
typ ─────┘└────────────────────────┘┴ └──────────────┘┴└┘└┘
doc ─────┘ ┴ └──────────────┘┴ └┘
txt ─────┘ ┴ ┴ └┘
par ─────┘ ┴ ┴ └┘
pid ─────┘ ┴ ┴ └┘
st ─────────────────────────────────────────────────────┘└──
645 { exact inf_edist_le_inf_edist_add_Hausdorff_edist },
id └────────────────────────────────────────┘
src └────┘└────────────────────────────────────────┘┴
typ └────┘└────────────────────────────────────────┘┴
doc └────┘└────────────────────────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└───────────────────────────────────────────────┘└┘└
646 { exact ennreal.add_ne_top.2 ⟨inf_edist_ne_top hs, fin⟩ }
id └────────────────┘ └──────────────┘ └┘ └─┘
src └────┘└────────────────┘└─┘ └──────────────┘┴ └┘└─┘└┘
typ └────┘└────────────────┘└─┘ └──────────────┘┴└┘└┘└─┘└┘
doc └────┘ └─┘ └──────────────┘┴ └┘ └┘
txt └────┘ └─┘ ┴ └┘ └┘
par └────┘ └─┘ ┴ └┘ └┘
pid ┴ └─┘ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────────────┘└─
647 end
st ──┘
648
649 /-- The Hausdorff distance is invariant under isometries -/
650 lemma Hausdorff_dist_image (h : isometry Φ) :
id └──────┘ ┴
src └──────┘
typ └──────┘ ┴
doc └──────┘
651 Hausdorff_dist (Φ '' s) (Φ '' t) = Hausdorff_dist s t :=
id └────────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ └┘ └┘ ┴ └────────────┘
typ └────────────┘ ┴ └┘ ┴ ┴ └┘ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘ └────────────┘
652 by simp [Hausdorff_dist, Hausdorff_edist_image h]
id └────────────┘ └───────────────────┘ ┴
src └────┘└────────────┘└┘└───────────────────┘┴ └─
typ └────┘└────────────┘└┘└───────────────────┘┴┴└─
doc └────┘└────────────┘└┘└───────────────────┘┴ └─
txt └────┘ └┘ ┴ └─
par └────┘ └┘ ┴ └─
pid ┴┴ └┘ ┴ ┴└
st └───────────────────────────────────────────────
653
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
654 /-- The Hausdorff distance satisfies the triangular inequality -/
655 lemma Hausdorff_dist_triangle (fin : Hausdorff_edist s t ≠ ⊤) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
656 Hausdorff_dist s u ≤ Hausdorff_dist s t + Hausdorff_dist t u :=
id └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ ┴ └────────────┘ ┴ └────────────┘
typ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘ └────────────┘ └────────────┘
657 begin
st └─────
658 by_cases Hausdorff_edist s u = ⊤,
id └─────────────┘ ┴ ┴ ┴ ┴
src └───────┘└─────────────┘┴ ┴ ┴┴┴┴
typ └───────┘└─────────────┘┴┴┴┴┴┴┴┴
doc └───────┘└─────────────┘┴ ┴ ┴ ┴
txt └───────┘ ┴ ┴ ┴ ┴
par └───────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────┘└─
659 { calc Hausdorff_dist s u = 0 + 0 : by simp [Hausdorff_dist, h]
id └──┘ ┴ └────────────┘ ┴
src └──┘ ┴ └────┘└────────────┘└┘ └─
typ └──┘ ┴ └────┘└────────────┘└┘┴└─
doc └──┘ └────┘└────────────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st ───┘└──────────────────────────────────┘└─────────────────────────
660 ... ≤ Hausdorff_dist s t + Hausdorff_dist t u :
id ┴ └────────────┘ ┴ ┴
src ────────┘ └────────────┘
typ ────────┘ ┴ └────────────┘ ┴ ┴
doc ────────┘ └────────────┘
txt ────────┘
par ────────┘
pid ────────┘
st ────────┘└───────────────────────────────────────────────
661 add_le_add (Hausdorff_dist_nonneg) (Hausdorff_dist_nonneg) },
id └────────┘ └───────────────────┘
src └────────┘ └───────────────────┘
typ └────────┘ └───────────────────┘
doc └───────────────────┘
st ────────────────────────────────────────────────────────────────────┘└─┘└
662 { have Dtu : Hausdorff_edist t u < ⊤ := calc
id └─────────────┘ ┴ ┴ ┴
src └─────────┘└─────────────┘┴ ┴ ┴┴┴ └──┘ └
typ └─────────┘└─────────────┘┴┴┴┴┴┴┴ └──┘ └
doc └─────────┘└─────────────┘┴ ┴ ┴ ┴ └──┘ └
txt └─────────┘ ┴ ┴ ┴ ┴ └──┘ └
par └─────────┘ ┴ ┴ ┴ ┴ └──┘ └
pid └──────┘└─┘ ┴ ┴ ┴ ┴ └──┘ └
st ───────────────────────────────────────────────
663 Hausdorff_edist t u ≤ Hausdorff_edist t s + Hausdorff_edist s u : Hausdorff_edist_triangle
id ┴ └─────────────┘ ┴ ┴ └──────────────────────┘
src ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └─┘└──────────────────────┘└
typ ─────┘ ┴ ┴ ┴ ┴ ┴┴┴ ┴ ┴└─────────────┘┴┴┴┴└─┘└──────────────────────┘└
doc ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└─────────────┘┴ ┴ └─┘└──────────────────────┘└
txt ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
par ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
pid ─────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └
st ─────────────────────────────────────────────────────────────────────────────────────────────────
664 ... = Hausdorff_edist s t + Hausdorff_edist s u : by simp [Hausdorff_edist_comm]
id └──────────────────┘
src ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└──────────────────┘└─
typ ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└──────────────────┘└─
doc ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘└──────────────────┘└─
txt ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └─
par ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴└────┘ └─
pid ─────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ └─────┘ └─
st ─────────────────────────────────────────────────────────┘└────────────────────────────
665 ... < ⊤ : by simp [ennreal.add_lt_top]; simp [ennreal.lt_top_iff_ne_top, h, fin],
id └────────────────┘ └───────────────────────┘ ┴ └─┘
src ─────┘└──┘ ┴ └─┘ ┴└─────┘└────────────────┘┴└┘└────┘└───────────────────────┘└┘ └┘└─┘┴
typ ─────┘└──┘ ┴ └─┘ ┴└─────┘└────────────────┘┴└┘└────┘└───────────────────────┘└┘┴└┘└─┘┴
doc ─────┘└──┘ ┴ └─┘ ┴└─────┘ ┴└┘└────┘ └┘ └┘ ┴
txt ─────┘└──┘ ┴ └─┘ ┴└─────┘ ┴└┘└────┘ └┘ └┘ ┴
par ─────┘└──┘ ┴ └─┘ ┴└─────┘ ┴└┘└────┘ └┘ └┘ ┴
pid ─────────┘ ┴ └─┘ └──────┘ └───────┘ └┘ └┘ ┴
st ─────┘└──────────┘└───────────────────────────────────────────────────────────────────┘└─
666 rw [Hausdorff_dist, Hausdorff_dist, Hausdorff_dist,
id └────────────┘ └────────────┘ └────────────┘
src └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
typ └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
doc └──┘└────────────┘└┘└────────────┘└┘└────────────┘└─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ └─
st ─────────────────────┘└──────────────┘└──────────────┘└─
667 ← ennreal.to_real_add fin (lt_top_iff_ne_top.1 Dtu), ennreal.to_real_le_to_real h],
id └─────────────────┘ └─┘ └───────────────┘ └─┘ └────────────────────────┘ ┴
src ─────────┘└─────────────────┘┴└─┘┴ └───────────────┘└─┘ └─┘└────────────────────────┘┴ ┴
typ ─────────┘└─────────────────┘┴└─┘┴ └───────────────┘└─┘└─┘└─┘└────────────────────────┘┴┴┴
doc ─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴
txt ─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴
par ─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴
pid ─────────┘ ┴ ┴ └─┘ └─┘ ┴ ┴
st ──────────────────────────────────────────────────────────┘└────────────────────────────┘└──
668 { exact Hausdorff_edist_triangle },
id └──────────────────────┘
src └────┘└──────────────────────┘┴
typ └────┘└──────────────────────┘┴
doc └────┘└──────────────────────┘┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ─────┘└─────────────────────────────┘└┘└
669 { simp [ennreal.add_eq_top, lt_top_iff_ne_top.1 Dtu, fin] }}
id └────────────────┘ └───────────────┘ └─┘ └─┘
src └────┘└────────────────┘└┘└───────────────┘└─┘ └┘└─┘└┘
typ └────┘└────────────────┘└┘└───────────────┘└─┘└─┘└┘└─┘└┘
doc └────┘ └┘ └─┘ └┘ └┘
txt └────┘ └┘ └─┘ └┘ └┘
par └────┘ └┘ └─┘ └┘ └┘
pid ┴┴ └┘ └─┘ └┘ ┴┴
st ─────────────────────────────────────────────────────────────┘└──
670 end
st ──┘
671
672 /-- The Hausdorff distance satisfies the triangular inequality -/
673 lemma Hausdorff_dist_triangle' (fin : Hausdorff_edist t u ≠ ⊤) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
674 Hausdorff_dist s u ≤ Hausdorff_dist s t + Hausdorff_dist t u :=
id └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ ┴ └────────────┘ ┴ └────────────┘
typ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └────────────┘ └────────────┘ └────────────┘
675 begin
st └─────
676 rw Hausdorff_edist_comm at fin,
id └──────────────────┘
src └─┘└──────────────────┘└─────┘
typ └─┘└──────────────────┘└─────┘
doc └─┘└──────────────────┘└─────┘
txt └─┘ └─────┘
par └─┘ └─────┘
pid ┴ └─────┘
st ───────────────────────────────┘└─
677 have I : Hausdorff_dist u s ≤ Hausdorff_dist u t + Hausdorff_dist t s := Hausdorff_dist_triangle fin,
id ┴ ┴ ┴ └────────────┘ ┴ ┴ └─────────────────────┘ └─┘
src └───────┘ ┴ ┴ ┴┴┴ ┴ ┴ ┴┴┴└────────────┘┴ ┴ └──┘└─────────────────────┘┴└─┘
typ └───────┘ ┴ ┴ ┴┴┴ ┴┴┴ ┴┴┴└────────────┘┴┴┴┴└──┘└─────────────────────┘┴└─┘
doc └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴└────────────┘┴ ┴ └──┘└─────────────────────┘┴
txt └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
par └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
pid └────┘└─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └──┘ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
678 simpa [add_comm, Hausdorff_dist_comm] using I
id └──────┘ └─────────────────┘ ┴
src └─────┘└──────┘└┘└─────────────────┘└──────┘ ┴
typ └─────┘└──────┘└┘└─────────────────┘└──────┘┴┴
doc └─────┘ └┘└─────────────────┘└──────┘ ┴
txt └─────┘ └┘ └──────┘ ┴
par └─────┘ └┘ └──────┘ ┴
pid ┴┴ └┘ ┴┴└────┘ ┴
st ───────────────────────────────────────────────┘
679 end
st └─┘
680
681 /-- The Hausdorff distance between a set and its closure vanish -/
682 @[simp] lemma Hausdorff_dist_self_closure : Hausdorff_dist s (closure s) = 0 :=
id └────────────┘ ┴ └─────┘ ┴ ┴
src └────────────┘ └─────┘ ┴
typ └────────────┘ ┴ └─────┘ ┴ ┴
doc └──┘ └────────────┘ └─────┘
683 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
684
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
685 /-- Replacing a set by its closure does not change the Hausdorff distance. -/
686 @[simp] lemma Hausdorff_dist_closure₁ : Hausdorff_dist (closure s) t = Hausdorff_dist s t :=
id └────────────┘ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ └─────┘ ┴ └────────────┘
typ └────────────┘ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴
doc └──┘ └────────────┘ └─────┘ └────────────┘
687 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
688
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
689 /-- Replacing a set by its closure does not change the Hausdorff distance. -/
690 @[simp] lemma Hausdorff_dist_closure₂ : Hausdorff_dist s (closure t) = Hausdorff_dist s t :=
id └────────────┘ ┴ └─────┘ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ └─────┘ ┴ └────────────┘
typ └────────────┘ ┴ └─────┘ ┴ ┴ └────────────┘ ┴ ┴
doc └──┘ └────────────┘ └─────┘ └────────────┘
691 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
692
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
693 /-- The Hausdorff distance between two sets and their closures coincide -/
694 @[simp] lemma Hausdorff_dist_closure : Hausdorff_dist (closure s) (closure t) = Hausdorff_dist s t :=
id └────────────┘ └─────┘ ┴ └─────┘ ┴ ┴ └────────────┘ ┴ ┴
src └────────────┘ └─────┘ └─────┘ ┴ └────────────┘
typ └────────────┘ └─────┘ ┴ └─────┘ ┴ ┴ └────────────┘ ┴ ┴
doc └──┘ └────────────┘ └─────┘ └─────┘ └────────────┘
695 by simp [Hausdorff_dist]
id └────────────┘
src └────┘└────────────┘└─
typ └────┘└────────────┘└─
doc └────┘└────────────┘└─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────────────────
696
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
697 /-- Two sets are at zero Hausdorff distance if and only if they have the same closures -/
698 lemma Hausdorff_dist_zero_iff_closure_eq_closure (fin : Hausdorff_edist s t ≠ ⊤) :
id └─────────────┘ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴
doc └─────────────┘
699 Hausdorff_dist s t = 0 ↔ closure s = closure t :=
id └────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
src └────────────┘ ┴ ┴ └─────┘ ┴ └─────┘
typ └────────────┘ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─────┘ ┴
doc └────────────┘ └─────┘ └─────┘
700 by simp [Hausdorff_edist_zero_iff_closure_eq_closure.symm, Hausdorff_dist,
id └────────────┘
src └────┘ └┘└────────────┘└─
typ └────┘└──────────────────────────────────────────────┘└┘└────────────┘└─
doc └────┘ └┘└────────────┘└─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ └─
st └────────────────────────────────────────────────────────────────────────
701 ennreal.to_real_eq_zero_iff, fin]
id └─────────────────────────┘ └─┘
src ────────┘└─────────────────────────┘└┘└─┘└─
typ ────────┘└─────────────────────────┘└┘└─┘└─
doc ────────┘ └┘ └─
txt ────────┘ └┘ └─
par ────────┘ └┘ └─
pid ────────┘ └┘ ┴└
st ───────────────────────────────────────────
702
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
703 /-- Two closed sets are at zero Hausdorff distance if and only if they coincide -/
704 lemma Hausdorff_dist_zero_iff_eq_of_closed (hs : is_closed s) (ht : is_closed t)
id └───────┘ ┴ └───────┘ ┴
src └───────┘ └───────┘
typ └───────┘ ┴ └───────┘ ┴
doc └───────┘ └───────┘
705 (fin : Hausdorff_edist s t ≠ ⊤) : Hausdorff_dist s t = 0 ↔ s = t :=
id └─────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─────────────┘ ┴ ┴ └────────────┘ ┴ ┴ ┴
typ └─────────────┘ ┴ ┴ ┴ ┴ └────────────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └─────────────┘ └────────────┘
706 by simp [(Hausdorff_edist_zero_iff_eq_of_closed hs ht).symm, Hausdorff_dist,
id └───────────────────────────────────┘ └┘ └┘ └────────────┘
src └────┘ └───────────────────────────────────┘┴ ┴ └──────┘└────────────┘└─
typ └────┘ └───────────────────────────────────┘┴└┘┴└┘└──────┘└────────────┘└─
doc └────┘ └───────────────────────────────────┘┴ ┴ └──────┘└────────────┘└─
txt └────┘ ┴ ┴ └──────┘ └─
par └────┘ ┴ ┴ └──────┘ └─
pid ┴┴ ┴ ┴ └──────┘ └─
st └──────────────────────────────────────────────────────────────────────────
707 ennreal.to_real_eq_zero_iff, fin]
id └─────────────────────────┘ └─┘
src ────────┘└─────────────────────────┘└┘└─┘└─
typ ────────┘└─────────────────────────┘└┘└─┘└─
doc ────────┘ └┘ └─
txt ────────┘ └┘ └─
par ────────┘ └┘ └─
pid ────────┘ └┘ ┴└
st ───────────────────────────────────────────
708
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
709 end --section
710 end metric --namespace